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

Theorem velsn 4342
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 3358 . 2 𝑥 ∈ V
21elsn 4341 1 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1634  wcel 2148  {csn 4326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-v 3357  df-sn 4327
This theorem is referenced by:  dfpr2  4345  ralsnsg  4365  rexsns  4366  disjsn  4394  snprc  4400  euabsn2  4407  snssg  4461  raldifsnb  4473  difprsnss  4476  pwpw0  4490  eqsn  4506  snsspw  4518  pwsnALT  4578  dfnfc2  4603  uni0b  4610  uni0c  4611  sndisj  4789  rext  5058  moabex  5069  exss  5073  otiunsndisj  5127  fconstmpt  5315  opeliunxp  5322  restidsing  5610  xpdifid  5714  dmsnopg  5759  sniota  6032  dfmpt3  6165  nfunsn  6383  dffv2  6430  fsn  6563  fnasrn  6572  fnsnb  6595  fmptsng  6597  fmptsnd  6598  fvclss  6662  eusvobj2  6805  suceloni  7181  opabex3d  7313  opabex3  7314  wfrlem14  7602  wfrlem15  7603  oarec  7817  ixp0x  8111  snmapen  8211  xpsnen  8221  marypha2lem2  8519  elirrv  8678  cantnfp1lem1  8760  cantnfp1lem3  8762  djuunxp  8968  dfac5lem1  9167  dfac5lem2  9168  dfac5lem4  9170  fin1a2lem11  9455  axdc4lem  9500  axcclem  9502  ttukeylem7  9560  xrsupexmnf  12359  xrinfmexpnf  12360  iccid  12444  fzsn  12612  fzpr  12625  seqz  13078  hashf1  13465  pr2pwpr  13485  s3iunsndisj  13939  fsum2dlem  14731  incexc2  14799  prodsn  14921  prodsnf  14923  fprod2dlem  14939  ef0lem  15037  lcmfunsnlem2  15582  1nprm  15620  vdwapun  15905  prmodvdslcmf  15978  cshwsiun  16033  xpsc0  16448  xpsc1  16449  mgmidsssn0  17497  mnd1id  17560  symg1bas  18043  pmtrprfvalrn  18135  gex1  18233  sylow2alem1  18259  lsmdisj2  18322  0frgp  18419  0cyg  18521  prmcyg  18522  dprddisj2  18666  ablfacrp  18693  kerf1hrm  18973  lspdisj  19358  lidlnz  19463  psrlidm  19638  mplcoe1  19700  mplcoe5  19703  evlslem1  19750  mulgrhm2  20082  ocvin  20255  maducoeval2  20684  madugsum  20687  en2top  21030  restsn  21215  ist1-3  21394  ordtt1  21424  cmpcld  21446  unisngl  21571  dissnlocfin  21573  ptopn2  21628  snfil  21908  alexsubALTlem2  22092  alexsubALTlem3  22093  alexsubALTlem4  22094  haustsms2  22180  tsmsxplem1  22196  tsmsxplem2  22197  ust0  22263  dscopn  22618  nmoid  22786  limcdif  23881  ellimc2  23882  limcmpt  23888  limcres  23891  ply1remlem  24163  plyeq0lem  24207  plyremlem  24300  aaliou2  24336  radcnv0  24411  abelthlem2  24427  wilthlem2  25037  vmappw  25084  ppinprm  25120  chtnprm  25122  musumsum  25160  dchrhash  25238  lgsquadlem1  25347  lgsquadlem2  25348  cplgr1v  26582  rusgrnumwwlkb0  27141  frgrncvvdeq  27512  fusgr2wsp2nb  27537  hsn0elch  28462  xrge0iifiso  30338  qqhval2  30383  esumnul  30467  esumrnmpt2  30487  esumfzf  30488  sibfof  30759  sitgaddlemb  30767  plymulx0  30981  signstf0  31002  signstfvneq0  31006  prodfzo03  31038  circlemeth  31075  bnj521  31160  sconnpi1  31576  dffr5  31998  eqfunresadj  32014  elima4  32032  brsingle  32378  dfiota3  32384  funpartfun  32404  dfrdg4  32412  fwddifn0  32625  bj-csbsnlem  33244  bj-restsn  33384  bj-rest10  33390  bj-raldifsn  33403  mptsnunlem  33539  matunitlindflem1  33755  poimirlem23  33782  poimirlem26  33785  poimirlem27  33786  grposnOLD  34029  0idl  34172  smprngopr  34199  isdmn3  34221  lshpdisj  34811  lsat0cv  34857  snatpsubN  35574  dibelval3  36972  dib1dim  36990  dvh2dim  37270  mapd0  37490  hdmap14lem13  37705  pellexlem5  37938  jm2.23  38104  flcidc  38285  snhesn  38620  snssiALTVD  39596  snssiALT  39597  fsneq  39927  iccintsng  40274  icoiccdif  40275  limcrecl  40385  lptioo2  40387  lptioo1  40388  limcresiooub  40398  limcresioolb  40399  cnrefiisplem  40579  icccncfext  40624  dvmptfprodlem  40683  dvnprodlem3  40687  dirkercncflem2  40844  fourierdlem40  40887  fourierdlem48  40894  fourierdlem51  40897  fourierdlem62  40908  fourierdlem66  40912  fourierdlem74  40920  fourierdlem75  40921  fourierdlem76  40922  fourierdlem78  40924  fourierdlem79  40925  fourierdlem93  40939  fourierdlem101  40947  fourierdlem103  40949  fourierdlem104  40950  fouriersw  40971  elaa2  40974  etransclem44  41018  rrxsnicc  41043  sge00  41116  absnsb  41695  funressnfv  41753  dfdfat2  41756  tz6.12-afv  41798  otiunsndisjX  41845  iccpartgtl  41914  iccpartgt  41915  iccpartleu  41916  iccpartgel  41917  nnsum4primeseven  42240  nnsum4primesevenALTV  42241  bgoldbtbnd  42249  xpsnopab  42317  opeliun2xp  42663  aacllem  43102
  Copyright terms: Public domain W3C validator