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

Theorem elsn 3559
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 3550 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2356 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    e. wcel 1621   {csn 3544
This theorem is referenced by:  dfpr2  3560  ralsns  3574  rexsns  3575  disjsn  3597  snprc  3599  euabsn2  3602  snss  3652  difprsn  3658  pwpw0  3663  eqsn  3675  snsspw  3684  pwsnALT  3722  dfnfc2  3745  uni0b  3750  uni0c  3751  sndisj  3912  rext  4116  moabex  4126  exss  4129  trsuc2OLD  4370  reusv6OLD  4436  suceloni  4495  fconstmpt  4639  opeliunxp  4647  dmsnopg  5050  dfmpt3  5223  nfunsn  5410  dffv2  5444  fsn  5548  fnasrn  5554  fconstfv  5586  fvclss  5612  opabex3  5621  eusvobj2  6223  oarec  6446  ixp0x  6730  xpsnen  6831  marypha2lem2  7073  elirrv  7195  sucprcreg  7197  cantnfp1lem1  7264  cantnfp1lem3  7266  dfac5lem1  7634  dfac5lem2  7635  dfac5lem4  7637  fin1a2lem11  7920  axdc4lem  7965  axcclem  7967  xrsupexmnf  10501  xrinfmexpnf  10502  iccid  10579  fzsn  10711  fzpr  10718  seqz  10972  hashf1  11272  fsum2dlem  12110  ef0lem  12234  divalgmod  12479  1nprm  12637  isprm2lem  12639  vdwapun  12895  xpsc0  13336  xpsc1  13337  gsumvallem1  14283  gex1  14737  sylow2alem1  14763  lsmdisj2  14826  0frgp  14923  0cyg  15014  prmcyg  15015  dprddisj2  15109  ablfacrp  15136  lspdisj  15713  lidlnz  15812  psrlidm  15980  mplcoe1  16041  mplcoe2  16043  mulgrhm2  16293  ocvin  16406  en2top  16555  restsn  16733  ist1-3  16909  ordtt1  16939  cmpcld  16961  ptopn2  17111  snfil  17391  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALTlem4  17576  haustsms2  17651  tsmsxplem1  17667  tsmsxplem2  17668  dscopn  17928  nmoid  18083  limcdif  19058  ellimc2  19059  limcmpt  19065  limcres  19068  evlslem1  19231  ply1remlem  19380  plyeq0lem  19424  plyremlem  19516  aaliou2  19552  radcnv0  19624  abelthlem2  19640  wilthlem2  20139  vmappw  20186  ppinprm  20222  chtnprm  20224  musumsum  20264  dchrhash  20342  lgsquadlem1  20425  lgsquadlem2  20426  grposn  20712  ablosn  20844  hsn0elch  21657  sconpi1  22941  ghomsn  23166  dffr5  23280  wfrlem14  23437  wfrlem15  23438  brsingle  23630  dfiota3  23636  funpartfun  23655  funpartfv  23657  dfrdg4  23662  fates  24120  restidsing  24241  pgapspf  25218  0idl  25816  smprngopr  25843  isdmn3  25865  pellexlem5  26084  jm2.23  26255  flcidc  26545  snssiALTVD  27292  snssiALT  27293  bnj145  27444  bnj521  27454  lshpdisj  27936  lsat0cv  27982  snatpsubN  28698  dibelval3  30096  dib1dim  30114  dvh2dim  30394  mapd0  30614  hdmap14lem13  30832
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 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-sn 3550
  Copyright terms: Public domain W3C validator