MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsn Unicode version

Theorem elsn 3656
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
elsn  |-  ( x  e.  { A }  <->  x  =  A )
Distinct variable group:    x, A

Proof of Theorem elsn
StepHypRef Expression
1 df-sn 3647 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2391 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1685   {csn 3641
This theorem is referenced by:  dfpr2  3657  ralsns  3671  rexsns  3672  disjsn  3694  snprc  3696  euabsn2  3699  snss  3749  difprsn  3757  pwpw0  3764  eqsn  3776  snsspw  3785  pwsnALT  3823  dfnfc2  3846  uni0b  3853  uni0c  3854  sndisj  4016  rext  4221  moabex  4231  exss  4235  trsuc2OLD  4476  reusv6OLD  4544  suceloni  4603  fconstmpt  4731  opeliunxp  4739  dmsnopg  5142  dfmpt3  5332  nfunsn  5520  dffv2  5554  fsn  5658  fnasrn  5664  fconstfv  5696  fvclss  5722  opabex3  5731  eusvobj2  6333  oarec  6556  ixp0x  6840  xpsnen  6942  marypha2lem2  7185  elirrv  7307  sucprcreg  7309  cantnfp1lem1  7376  cantnfp1lem3  7378  dfac5lem1  7746  dfac5lem2  7747  dfac5lem4  7749  fin1a2lem11  8032  axdc4lem  8077  axcclem  8079  xrsupexmnf  10619  xrinfmexpnf  10620  iccid  10697  fzsn  10829  fzpr  10836  seqz  11090  hashf1  11391  fsum2dlem  12229  incexc2  12293  ef0lem  12356  divalgmod  12601  1nprm  12759  isprm2lem  12761  vdwapun  13017  xpsc0  13458  xpsc1  13459  gsumvallem1  14444  gex1  14898  sylow2alem1  14924  lsmdisj2  14987  0frgp  15084  0cyg  15175  prmcyg  15176  dprddisj2  15270  ablfacrp  15297  lspdisj  15874  lidlnz  15976  psrlidm  16144  mplcoe1  16205  mplcoe2  16207  mulgrhm2  16457  ocvin  16570  en2top  16719  restsn  16897  ist1-3  17073  ordtt1  17103  cmpcld  17125  ptopn2  17275  snfil  17555  alexsubALTlem2  17738  alexsubALTlem3  17739  alexsubALTlem4  17740  haustsms2  17815  tsmsxplem1  17831  tsmsxplem2  17832  dscopn  18092  nmoid  18247  limcdif  19222  ellimc2  19223  limcmpt  19229  limcres  19232  evlslem1  19395  ply1remlem  19544  plyeq0lem  19588  plyremlem  19680  aaliou2  19716  radcnv0  19788  abelthlem2  19804  wilthlem2  20303  vmappw  20350  ppinprm  20386  chtnprm  20388  musumsum  20428  dchrhash  20506  lgsquadlem1  20589  lgsquadlem2  20590  grposn  20876  ablosn  21008  hsn0elch  21823  sconpi1  23177  ghomsn  23402  dffr5  23516  wfrlem14  23673  wfrlem15  23674  brsingle  23866  dfiota3  23872  funpartfun  23891  funpartfv  23893  dfrdg4  23898  fates  24365  restidsing  24486  pgapspf  25463  0idl  26061  smprngopr  26088  isdmn3  26110  pellexlem5  26329  jm2.23  26500  flcidc  26790  funressnfv  27382  dfdfat2  27385  tz6.12-afv  27426  snssiALTVD  27882  snssiALT  27883  bnj145  28034  bnj521  28044  lshpdisj  28456  lsat0cv  28502  snatpsubN  29218  dibelval3  30616  dib1dim  30634  dvh2dim  30914  mapd0  31134  hdmap14lem13  31352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-sn 3647
  Copyright terms: Public domain W3C validator