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

Theorem elsn 3793
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 3784 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2515 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1721   {csn 3778
This theorem is referenced by:  dfpr2  3794  ralsns  3808  rexsns  3809  disjsn  3832  snprc  3835  euabsn2  3839  snss  3890  difprsnss  3898  pwpw0  3910  eqsn  3924  snsspw  3934  pwsnALT  3974  dfnfc2  3997  uni0b  4004  uni0c  4005  sndisj  4168  rext  4376  moabex  4386  exss  4390  reusv6OLD  4697  suceloni  4756  fconstmpt  4884  opeliunxp  4892  dmsnopg  5304  dfmpt3  5530  nfunsn  5724  dffv2  5759  fsn  5869  fnasrn  5875  fconstfv  5917  fvclss  5943  opabex3d  5952  opabex3  5953  eusvobj2  6545  oarec  6768  ixp0x  7053  xpsnen  7155  marypha2lem2  7403  elirrv  7525  sucprcreg  7527  cantnfp1lem1  7594  cantnfp1lem3  7596  dfac5lem1  7964  dfac5lem2  7965  dfac5lem4  7967  fin1a2lem11  8250  axdc4lem  8295  axcclem  8297  xrsupexmnf  10843  xrinfmexpnf  10844  iccid  10921  fzsn  11054  fzpr  11061  seqz  11330  hashf1  11665  fsum2dlem  12513  incexc2  12577  ef0lem  12640  divalgmod  12885  1nprm  13043  isprm2lem  13045  vdwapun  13301  xpsc0  13744  xpsc1  13745  gsumvallem1  14730  gex1  15184  sylow2alem1  15210  lsmdisj2  15273  0frgp  15370  0cyg  15461  prmcyg  15462  dprddisj2  15556  ablfacrp  15583  lspdisj  16156  lidlnz  16258  psrlidm  16426  mplcoe1  16487  mplcoe2  16489  mulgrhm2  16747  ocvin  16860  en2top  17009  restsn  17192  ist1-3  17371  ordtt1  17401  cmpcld  17423  ptopn2  17573  snfil  17853  alexsubALTlem2  18036  alexsubALTlem3  18037  alexsubALTlem4  18038  haustsms2  18123  tsmsxplem1  18139  tsmsxplem2  18140  ust0  18206  dscopn  18578  nmoid  18733  limcdif  19720  ellimc2  19721  limcmpt  19727  limcres  19730  evlslem1  19893  ply1remlem  20042  plyeq0lem  20086  plyremlem  20178  aaliou2  20214  radcnv0  20289  abelthlem2  20305  wilthlem2  20809  vmappw  20856  ppinprm  20892  chtnprm  20894  musumsum  20934  dchrhash  21012  lgsquadlem1  21095  lgsquadlem2  21096  isusgra0  21333  nbcusgra  21429  usgrasscusgra  21449  grposn  21760  ablosn  21892  hsn0elch  22707  kerf1hrm  24219  xrge0iifiso  24278  qqhval2  24323  esumnul  24400  esumfzf  24416  sibfof  24611  sconpi1  24883  ghomsn  25056  prodsn  25243  fprod2dlem  25261  dffr5  25328  wfrlem14  25487  wfrlem15  25488  brsingle  25674  dfiota3  25680  funpartfun  25700  dfrdg4  25707  0idl  26529  smprngopr  26556  isdmn3  26578  pellexlem5  26790  jm2.23  26961  flcidc  27251  funressnfv  27863  dfdfat2  27866  tz6.12-afv  27908  raldifsnb  27950  otiunsndisj  27958  otiunsndisjX  27959  frgrancvvdeqlem9  28148  frgrawopreglem4  28154  usg2spot2nb  28172  snssiALTVD  28652  snssiALT  28653  bnj145  28804  bnj521  28814  lshpdisj  29474  lsat0cv  29520  snatpsubN  30236  dibelval3  31634  dib1dim  31652  dvh2dim  31932  mapd0  32152  hdmap14lem13  32370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-sn 3784
  Copyright terms: Public domain W3C validator