MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  velsn Structured version   Visualization version   GIF version

Theorem velsn 4226
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
velsn (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)

Proof of Theorem velsn
StepHypRef Expression
1 vex 3234 . 2 𝑥 ∈ V
21elsn 4225 1 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sn 4211
This theorem is referenced by:  dfpr2  4228  ralsnsg  4248  rexsns  4249  disjsn  4278  snprc  4285  euabsn2  4292  snssg  4347  raldifsnb  4358  difprsnss  4361  pwpw0  4376  eqsn  4393  eqsnOLD  4394  snsspw  4407  pwsnALT  4461  dfnfc2  4486  dfnfc2OLD  4487  uni0b  4495  uni0c  4496  sndisj  4676  rext  4946  moabex  4957  exss  4961  otiunsndisj  5009  fconstmpt  5197  opeliunxp  5204  restidsing  5493  restidsingOLD  5494  xpdifid  5597  dmsnopg  5642  elsnxpOLD  5716  sniota  5916  dfmpt3  6052  nfunsn  6263  dffv2  6310  fsn  6442  fnasrn  6451  fnsnb  6473  fmptsng  6475  fmptsnd  6476  fvclss  6540  eusvobj2  6683  suceloni  7055  opabex3d  7187  opabex3  7188  wfrlem14  7473  wfrlem15  7474  oarec  7687  ixp0x  7978  xpsnen  8085  marypha2lem2  8383  elirrv  8542  cantnfp1lem1  8613  cantnfp1lem3  8615  dfac5lem1  8984  dfac5lem2  8985  dfac5lem4  8987  fin1a2lem11  9270  axdc4lem  9315  axcclem  9317  ttukeylem7  9375  xrsupexmnf  12173  xrinfmexpnf  12174  iccid  12258  fzsn  12421  fzpr  12434  seqz  12889  hashf1  13279  pr2pwpr  13299  s3iunsndisj  13753  fsum2dlem  14545  incexc2  14614  prodsn  14736  prodsnf  14738  fprod2dlem  14754  ef0lem  14853  divalgmodOLD  15177  lcmfunsnlem2  15400  1nprm  15439  vdwapun  15725  prmodvdslcmf  15798  cshwsiun  15853  xpsc0  16267  xpsc1  16268  mgmidsssn0  17316  mnd1id  17379  symg1bas  17862  pmtrprfvalrn  17954  gex1  18052  sylow2alem1  18078  lsmdisj2  18141  0frgp  18238  0cyg  18340  prmcyg  18341  dprddisj2  18484  ablfacrp  18511  kerf1hrm  18791  lspdisj  19173  lidlnz  19276  psrlidm  19451  mplcoe1  19513  mplcoe5  19516  evlslem1  19563  mulgrhm2  19895  ocvin  20066  maducoeval2  20494  madugsum  20497  en2top  20837  restsn  21022  ist1-3  21201  ordtt1  21231  cmpcld  21253  unisngl  21378  dissnlocfin  21380  ptopn2  21435  snfil  21715  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  haustsms2  21987  tsmsxplem1  22003  tsmsxplem2  22004  ust0  22070  dscopn  22425  nmoid  22593  limcdif  23685  ellimc2  23686  limcmpt  23692  limcres  23695  ply1remlem  23967  plyeq0lem  24011  plyremlem  24104  aaliou2  24140  radcnv0  24215  abelthlem2  24231  wilthlem2  24840  vmappw  24887  ppinprm  24923  chtnprm  24925  musumsum  24963  dchrhash  25041  lgsquadlem1  25150  lgsquadlem2  25151  cplgr1v  26382  rusgrnumwwlkb0  26938  frgrncvvdeq  27289  fusgr2wsp2nb  27314  hsn0elch  28233  xrge0iifiso  30109  qqhval2  30154  esumnul  30238  esumrnmpt2  30258  esumfzf  30259  sibfof  30530  sitgaddlemb  30538  plymulx0  30752  signstf0  30773  signstfvneq0  30777  prodfzo03  30809  circlemeth  30846  bnj521  30931  sconnpi1  31347  dffr5  31769  eqfunresadj  31785  elima4  31803  brsingle  32149  dfiota3  32155  funpartfun  32175  dfrdg4  32183  fwddifn0  32396  bj-csbsnlem  33023  bj-restsn  33160  bj-rest10  33166  bj-raldifsn  33179  mptsnunlem  33315  matunitlindflem1  33535  poimirlem23  33562  poimirlem26  33565  poimirlem27  33566  grposnOLD  33811  0idl  33954  smprngopr  33981  isdmn3  34003  lshpdisj  34592  lsat0cv  34638  snatpsubN  35354  dibelval3  36753  dib1dim  36771  dvh2dim  37051  mapd0  37271  hdmap14lem13  37489  pellexlem5  37714  jm2.23  37880  flcidc  38061  snhesn  38397  snssiALTVD  39376  snssiALT  39377  fsneq  39712  iccintsng  40067  icoiccdif  40068  limcrecl  40179  lptioo2  40181  lptioo1  40182  limcresiooub  40192  limcresioolb  40193  cnrefiisplem  40373  icccncfext  40418  dvmptfprodlem  40477  dvnprodlem3  40481  dirkercncflem2  40639  fourierdlem40  40682  fourierdlem48  40689  fourierdlem51  40692  fourierdlem62  40703  fourierdlem66  40707  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem93  40734  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  elaa2  40769  etransclem44  40813  rrxsnicc  40838  sge00  40911  funressnfv  41529  dfdfat2  41532  tz6.12-afv  41574  otiunsndisjX  41621  iccpartgtl  41687  iccpartgt  41688  iccpartleu  41689  iccpartgel  41690  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbnd  42022  xpsnopab  42090  opeliun2xp  42436  aacllem  42875
  Copyright terms: Public domain W3C validator