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

Theorem elsn 3629
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 3620 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2365 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    e. wcel 1621   {csn 3614
This theorem is referenced by:  dfpr2  3630  ralsns  3644  rexsns  3645  disjsn  3667  snprc  3669  euabsn2  3672  snss  3722  difprsn  3730  pwpw0  3737  eqsn  3749  snsspw  3758  pwsnALT  3796  dfnfc2  3819  uni0b  3826  uni0c  3827  sndisj  3989  rext  4194  moabex  4204  exss  4208  trsuc2OLD  4449  reusv6OLD  4517  suceloni  4576  fconstmpt  4720  opeliunxp  4728  dmsnopg  5131  dfmpt3  5304  nfunsn  5492  dffv2  5526  fsn  5630  fnasrn  5636  fconstfv  5668  fvclss  5694  opabex3  5703  eusvobj2  6305  oarec  6528  ixp0x  6812  xpsnen  6914  marypha2lem2  7157  elirrv  7279  sucprcreg  7281  cantnfp1lem1  7348  cantnfp1lem3  7350  dfac5lem1  7718  dfac5lem2  7719  dfac5lem4  7721  fin1a2lem11  8004  axdc4lem  8049  axcclem  8051  xrsupexmnf  10590  xrinfmexpnf  10591  iccid  10668  fzsn  10800  fzpr  10807  seqz  11061  hashf1  11361  fsum2dlem  12199  ef0lem  12323  divalgmod  12568  1nprm  12726  isprm2lem  12728  vdwapun  12984  xpsc0  13425  xpsc1  13426  gsumvallem1  14411  gex1  14865  sylow2alem1  14891  lsmdisj2  14954  0frgp  15051  0cyg  15142  prmcyg  15143  dprddisj2  15237  ablfacrp  15264  lspdisj  15841  lidlnz  15943  psrlidm  16111  mplcoe1  16172  mplcoe2  16174  mulgrhm2  16424  ocvin  16537  en2top  16686  restsn  16864  ist1-3  17040  ordtt1  17070  cmpcld  17092  ptopn2  17242  snfil  17522  alexsubALTlem2  17705  alexsubALTlem3  17706  alexsubALTlem4  17707  haustsms2  17782  tsmsxplem1  17798  tsmsxplem2  17799  dscopn  18059  nmoid  18214  limcdif  19189  ellimc2  19190  limcmpt  19196  limcres  19199  evlslem1  19362  ply1remlem  19511  plyeq0lem  19555  plyremlem  19647  aaliou2  19683  radcnv0  19755  abelthlem2  19771  wilthlem2  20270  vmappw  20317  ppinprm  20353  chtnprm  20355  musumsum  20395  dchrhash  20473  lgsquadlem1  20556  lgsquadlem2  20557  grposn  20843  ablosn  20975  hsn0elch  21788  sconpi1  23143  ghomsn  23368  dffr5  23482  wfrlem14  23639  wfrlem15  23640  brsingle  23832  dfiota3  23838  funpartfun  23857  funpartfv  23859  dfrdg4  23864  fates  24322  restidsing  24443  pgapspf  25420  0idl  26018  smprngopr  26045  isdmn3  26067  pellexlem5  26286  jm2.23  26457  flcidc  26747  snssiALTVD  27735  snssiALT  27736  bnj145  27887  bnj521  27897  lshpdisj  28427  lsat0cv  28473  snatpsubN  29189  dibelval3  30587  dib1dim  30605  dvh2dim  30885  mapd0  31105  hdmap14lem13  31323
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 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-sn 3620
  Copyright terms: Public domain W3C validator