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

Theorem elsn 3668
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 3659 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2403 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    e. wcel 1696   {csn 3653
This theorem is referenced by:  dfpr2  3669  ralsns  3683  rexsns  3684  disjsn  3706  snprc  3708  euabsn2  3711  snss  3761  difprsnss  3769  pwpw0  3779  eqsn  3791  snsspw  3800  pwsnALT  3838  dfnfc2  3861  uni0b  3868  uni0c  3869  sndisj  4031  rext  4238  moabex  4248  exss  4252  trsuc2OLD  4493  reusv6OLD  4561  suceloni  4620  fconstmpt  4748  opeliunxp  4756  dmsnopg  5160  dfmpt3  5382  nfunsn  5574  dffv2  5608  fsn  5712  fnasrn  5718  fconstfv  5750  fvclss  5776  opabex3  5785  eusvobj2  6353  oarec  6576  ixp0x  6860  xpsnen  6962  marypha2lem2  7205  elirrv  7327  sucprcreg  7329  cantnfp1lem1  7396  cantnfp1lem3  7398  dfac5lem1  7766  dfac5lem2  7767  dfac5lem4  7769  fin1a2lem11  8052  axdc4lem  8097  axcclem  8099  xrsupexmnf  10639  xrinfmexpnf  10640  iccid  10717  fzsn  10849  fzpr  10856  seqz  11110  hashf1  11411  fsum2dlem  12249  incexc2  12313  ef0lem  12376  divalgmod  12621  1nprm  12779  isprm2lem  12781  vdwapun  13037  xpsc0  13478  xpsc1  13479  gsumvallem1  14464  gex1  14918  sylow2alem1  14944  lsmdisj2  15007  0frgp  15104  0cyg  15195  prmcyg  15196  dprddisj2  15290  ablfacrp  15317  lspdisj  15894  lidlnz  15996  psrlidm  16164  mplcoe1  16225  mplcoe2  16227  mulgrhm2  16477  ocvin  16590  en2top  16739  restsn  16917  ist1-3  17093  ordtt1  17123  cmpcld  17145  ptopn2  17295  snfil  17575  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  haustsms2  17835  tsmsxplem1  17851  tsmsxplem2  17852  dscopn  18112  nmoid  18267  limcdif  19242  ellimc2  19243  limcmpt  19249  limcres  19252  evlslem1  19415  ply1remlem  19564  plyeq0lem  19608  plyremlem  19700  aaliou2  19736  radcnv0  19808  abelthlem2  19824  wilthlem2  20323  vmappw  20370  ppinprm  20406  chtnprm  20408  musumsum  20448  dchrhash  20526  lgsquadlem1  20609  lgsquadlem2  20610  grposn  20898  ablosn  21030  hsn0elch  21843  xrge0iifiso  23332  esumnul  23442  sconpi1  23785  ghomsn  24010  dffr5  24181  wfrlem14  24340  wfrlem15  24341  brsingle  24527  dfiota3  24533  funpartfun  24553  dfrdg4  24560  fates  25058  restidsing  25179  pgapspf  26155  0idl  26753  smprngopr  26780  isdmn3  26802  pellexlem5  27021  jm2.23  27192  flcidc  27482  funressnfv  28096  dfdfat2  28099  tz6.12-afv  28141  opabex3d  28190  isusgra0  28238  nbcusgra  28298  snssiALTVD  28918  snssiALT  28919  bnj145  29071  bnj521  29081  lshpdisj  29799  lsat0cv  29845  snatpsubN  30561  dibelval3  31959  dib1dim  31977  dvh2dim  32257  mapd0  32477  hdmap14lem13  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-sn 3659
  Copyright terms: Public domain W3C validator