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

Theorem elsn 3596
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 3587 . 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 3581
This theorem is referenced by:  dfpr2  3597  ralsns  3611  rexsns  3612  disjsn  3634  snprc  3636  euabsn2  3639  snss  3689  difprsn  3697  pwpw0  3704  eqsn  3716  snsspw  3725  pwsnALT  3763  dfnfc2  3786  uni0b  3793  uni0c  3794  sndisj  3955  rext  4160  moabex  4170  exss  4173  trsuc2OLD  4414  reusv6OLD  4482  suceloni  4541  fconstmpt  4685  opeliunxp  4693  dmsnopg  5096  dfmpt3  5269  nfunsn  5457  dffv2  5491  fsn  5595  fnasrn  5601  fconstfv  5633  fvclss  5659  opabex3  5668  eusvobj2  6270  oarec  6493  ixp0x  6777  xpsnen  6879  marypha2lem2  7122  elirrv  7244  sucprcreg  7246  cantnfp1lem1  7313  cantnfp1lem3  7315  dfac5lem1  7683  dfac5lem2  7684  dfac5lem4  7686  fin1a2lem11  7969  axdc4lem  8014  axcclem  8016  xrsupexmnf  10554  xrinfmexpnf  10555  iccid  10632  fzsn  10764  fzpr  10771  seqz  11025  hashf1  11325  fsum2dlem  12163  ef0lem  12287  divalgmod  12532  1nprm  12690  isprm2lem  12692  vdwapun  12948  xpsc0  13389  xpsc1  13390  gsumvallem1  14375  gex1  14829  sylow2alem1  14855  lsmdisj2  14918  0frgp  15015  0cyg  15106  prmcyg  15107  dprddisj2  15201  ablfacrp  15228  lspdisj  15805  lidlnz  15907  psrlidm  16075  mplcoe1  16136  mplcoe2  16138  mulgrhm2  16388  ocvin  16501  en2top  16650  restsn  16828  ist1-3  17004  ordtt1  17034  cmpcld  17056  ptopn2  17206  snfil  17486  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALTlem4  17671  haustsms2  17746  tsmsxplem1  17762  tsmsxplem2  17763  dscopn  18023  nmoid  18178  limcdif  19153  ellimc2  19154  limcmpt  19160  limcres  19163  evlslem1  19326  ply1remlem  19475  plyeq0lem  19519  plyremlem  19611  aaliou2  19647  radcnv0  19719  abelthlem2  19735  wilthlem2  20234  vmappw  20281  ppinprm  20317  chtnprm  20319  musumsum  20359  dchrhash  20437  lgsquadlem1  20520  lgsquadlem2  20521  grposn  20807  ablosn  20939  hsn0elch  21752  sconpi1  23107  ghomsn  23332  dffr5  23446  wfrlem14  23603  wfrlem15  23604  brsingle  23796  dfiota3  23802  funpartfun  23821  funpartfv  23823  dfrdg4  23828  fates  24286  restidsing  24407  pgapspf  25384  0idl  25982  smprngopr  26009  isdmn3  26031  pellexlem5  26250  jm2.23  26421  flcidc  26711  snssiALTVD  27615  snssiALT  27616  bnj145  27767  bnj521  27777  lshpdisj  28307  lsat0cv  28353  snatpsubN  29069  dibelval3  30467  dib1dim  30485  dvh2dim  30765  mapd0  30985  hdmap14lem13  31203
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 3587
  Copyright terms: Public domain W3C validator