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

Theorem elsn 3657
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 3648 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2392 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1625    e. wcel 1686   {csn 3642
This theorem is referenced by:  dfpr2  3658  ralsns  3672  rexsns  3673  disjsn  3695  snprc  3697  euabsn2  3700  snss  3750  difprsn  3758  pwpw0  3765  eqsn  3777  snsspw  3786  pwsnALT  3824  dfnfc2  3847  uni0b  3854  uni0c  3855  sndisj  4017  rext  4224  moabex  4234  exss  4238  trsuc2OLD  4479  reusv6OLD  4547  suceloni  4606  fconstmpt  4734  opeliunxp  4742  dmsnopg  5146  dfmpt3  5368  nfunsn  5560  dffv2  5594  fsn  5698  fnasrn  5704  fconstfv  5736  fvclss  5762  opabex3  5771  eusvobj2  6339  oarec  6562  ixp0x  6846  xpsnen  6948  marypha2lem2  7191  elirrv  7313  sucprcreg  7315  cantnfp1lem1  7382  cantnfp1lem3  7384  dfac5lem1  7752  dfac5lem2  7753  dfac5lem4  7755  fin1a2lem11  8038  axdc4lem  8083  axcclem  8085  xrsupexmnf  10625  xrinfmexpnf  10626  iccid  10703  fzsn  10835  fzpr  10842  seqz  11096  hashf1  11397  fsum2dlem  12235  incexc2  12299  ef0lem  12362  divalgmod  12607  1nprm  12765  isprm2lem  12767  vdwapun  13023  xpsc0  13464  xpsc1  13465  gsumvallem1  14450  gex1  14904  sylow2alem1  14930  lsmdisj2  14993  0frgp  15090  0cyg  15181  prmcyg  15182  dprddisj2  15276  ablfacrp  15303  lspdisj  15880  lidlnz  15982  psrlidm  16150  mplcoe1  16211  mplcoe2  16213  mulgrhm2  16463  ocvin  16576  en2top  16725  restsn  16903  ist1-3  17079  ordtt1  17109  cmpcld  17131  ptopn2  17281  snfil  17561  alexsubALTlem2  17744  alexsubALTlem3  17745  alexsubALTlem4  17746  haustsms2  17821  tsmsxplem1  17837  tsmsxplem2  17838  dscopn  18098  nmoid  18253  limcdif  19228  ellimc2  19229  limcmpt  19235  limcres  19238  evlslem1  19401  ply1remlem  19550  plyeq0lem  19594  plyremlem  19686  aaliou2  19722  radcnv0  19794  abelthlem2  19810  wilthlem2  20309  vmappw  20356  ppinprm  20392  chtnprm  20394  musumsum  20434  dchrhash  20512  lgsquadlem1  20595  lgsquadlem2  20596  grposn  20884  ablosn  21016  hsn0elch  21829  xrge0iifiso  23319  esumnul  23429  sconpi1  23772  ghomsn  23997  dffr5  24112  wfrlem14  24271  wfrlem15  24272  brsingle  24458  dfiota3  24464  funpartfun  24483  funpartfv  24485  dfrdg4  24490  fates  24966  restidsing  25087  pgapspf  26063  0idl  26661  smprngopr  26688  isdmn3  26710  pellexlem5  26929  jm2.23  27100  flcidc  27390  funressnfv  28002  dfdfat2  28005  tz6.12-afv  28046  isusgra0  28117  nbcusgra  28170  snssiALTVD  28675  snssiALT  28676  bnj145  28828  bnj521  28838  lshpdisj  29250  lsat0cv  29296  snatpsubN  30012  dibelval3  31410  dib1dim  31428  dvh2dim  31708  mapd0  31928  hdmap14lem13  32146
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-sn 3648
  Copyright terms: Public domain W3C validator