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

Theorem elsn 3615
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 3606 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2363 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    e. wcel 1621   {csn 3600
This theorem is referenced by:  dfpr2  3616  ralsns  3630  rexsns  3631  disjsn  3653  snprc  3655  euabsn2  3658  snss  3708  difprsn  3716  pwpw0  3723  eqsn  3735  snsspw  3744  pwsnALT  3782  dfnfc2  3805  uni0b  3812  uni0c  3813  sndisj  3975  rext  4180  moabex  4190  exss  4194  trsuc2OLD  4435  reusv6OLD  4503  suceloni  4562  fconstmpt  4706  opeliunxp  4714  dmsnopg  5117  dfmpt3  5290  nfunsn  5478  dffv2  5512  fsn  5616  fnasrn  5622  fconstfv  5654  fvclss  5680  opabex3  5689  eusvobj2  6291  oarec  6514  ixp0x  6798  xpsnen  6900  marypha2lem2  7143  elirrv  7265  sucprcreg  7267  cantnfp1lem1  7334  cantnfp1lem3  7336  dfac5lem1  7704  dfac5lem2  7705  dfac5lem4  7707  fin1a2lem11  7990  axdc4lem  8035  axcclem  8037  xrsupexmnf  10575  xrinfmexpnf  10576  iccid  10653  fzsn  10785  fzpr  10792  seqz  11046  hashf1  11346  fsum2dlem  12184  ef0lem  12308  divalgmod  12553  1nprm  12711  isprm2lem  12713  vdwapun  12969  xpsc0  13410  xpsc1  13411  gsumvallem1  14396  gex1  14850  sylow2alem1  14876  lsmdisj2  14939  0frgp  15036  0cyg  15127  prmcyg  15128  dprddisj2  15222  ablfacrp  15249  lspdisj  15826  lidlnz  15928  psrlidm  16096  mplcoe1  16157  mplcoe2  16159  mulgrhm2  16409  ocvin  16522  en2top  16671  restsn  16849  ist1-3  17025  ordtt1  17055  cmpcld  17077  ptopn2  17227  snfil  17507  alexsubALTlem2  17690  alexsubALTlem3  17691  alexsubALTlem4  17692  haustsms2  17767  tsmsxplem1  17783  tsmsxplem2  17784  dscopn  18044  nmoid  18199  limcdif  19174  ellimc2  19175  limcmpt  19181  limcres  19184  evlslem1  19347  ply1remlem  19496  plyeq0lem  19540  plyremlem  19632  aaliou2  19668  radcnv0  19740  abelthlem2  19756  wilthlem2  20255  vmappw  20302  ppinprm  20338  chtnprm  20340  musumsum  20380  dchrhash  20458  lgsquadlem1  20541  lgsquadlem2  20542  grposn  20828  ablosn  20960  hsn0elch  21773  sconpi1  23128  ghomsn  23353  dffr5  23467  wfrlem14  23624  wfrlem15  23625  brsingle  23817  dfiota3  23823  funpartfun  23842  funpartfv  23844  dfrdg4  23849  fates  24307  restidsing  24428  pgapspf  25405  0idl  26003  smprngopr  26030  isdmn3  26052  pellexlem5  26271  jm2.23  26442  flcidc  26732  snssiALTVD  27636  snssiALT  27637  bnj145  27788  bnj521  27798  lshpdisj  28328  lsat0cv  28374  snatpsubN  29090  dibelval3  30488  dib1dim  30506  dvh2dim  30786  mapd0  31006  hdmap14lem13  31224
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-sn 3606
  Copyright terms: Public domain W3C validator