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

Theorem elsn 3765
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 3756 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2487 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1717   {csn 3750
This theorem is referenced by:  dfpr2  3766  ralsns  3780  rexsns  3781  disjsn  3804  snprc  3807  euabsn2  3811  snss  3862  difprsnss  3870  pwpw0  3882  eqsn  3896  snsspw  3905  pwsnALT  3945  dfnfc2  3968  uni0b  3975  uni0c  3976  sndisj  4138  rext  4346  moabex  4356  exss  4360  reusv6OLD  4667  suceloni  4726  fconstmpt  4854  opeliunxp  4862  dmsnopg  5274  dfmpt3  5500  nfunsn  5694  dffv2  5728  fsn  5838  fnasrn  5844  fconstfv  5886  fvclss  5912  opabex3d  5921  opabex3  5922  eusvobj2  6511  oarec  6734  ixp0x  7019  xpsnen  7121  marypha2lem2  7369  elirrv  7491  sucprcreg  7493  cantnfp1lem1  7560  cantnfp1lem3  7562  dfac5lem1  7930  dfac5lem2  7931  dfac5lem4  7933  fin1a2lem11  8216  axdc4lem  8261  axcclem  8263  xrsupexmnf  10808  xrinfmexpnf  10809  iccid  10886  fzsn  11019  fzpr  11026  seqz  11291  hashf1  11626  fsum2dlem  12474  incexc2  12538  ef0lem  12601  divalgmod  12846  1nprm  13004  isprm2lem  13006  vdwapun  13262  xpsc0  13705  xpsc1  13706  gsumvallem1  14691  gex1  15145  sylow2alem1  15171  lsmdisj2  15234  0frgp  15331  0cyg  15422  prmcyg  15423  dprddisj2  15517  ablfacrp  15544  lspdisj  16117  lidlnz  16219  psrlidm  16387  mplcoe1  16448  mplcoe2  16450  mulgrhm2  16704  ocvin  16817  en2top  16966  restsn  17149  ist1-3  17328  ordtt1  17358  cmpcld  17380  ptopn2  17530  snfil  17810  alexsubALTlem2  17993  alexsubALTlem3  17994  alexsubALTlem4  17995  haustsms2  18080  tsmsxplem1  18096  tsmsxplem2  18097  ust0  18163  dscopn  18485  nmoid  18640  limcdif  19623  ellimc2  19624  limcmpt  19630  limcres  19633  evlslem1  19796  ply1remlem  19945  plyeq0lem  19989  plyremlem  20081  aaliou2  20117  radcnv0  20192  abelthlem2  20208  wilthlem2  20712  vmappw  20759  ppinprm  20795  chtnprm  20797  musumsum  20837  dchrhash  20915  lgsquadlem1  20998  lgsquadlem2  20999  isusgra0  21236  nbcusgra  21331  usgrasscusgra  21351  grposn  21644  ablosn  21776  hsn0elch  22591  kerf1hrm  24071  xrge0iifiso  24118  qqhval2  24158  esumnul  24232  esumfzf  24248  sconpi1  24698  ghomsn  24871  prodsn  25058  dffr5  25127  wfrlem14  25286  wfrlem15  25287  brsingle  25473  dfiota3  25479  funpartfun  25499  dfrdg4  25506  0idl  26319  smprngopr  26346  isdmn3  26368  pellexlem5  26580  jm2.23  26751  flcidc  27041  funressnfv  27654  dfdfat2  27657  tz6.12-afv  27699  frgrancvvdeqlem9  27786  frgrawopreglem4  27792  snssiALTVD  28273  snssiALT  28274  bnj145  28425  bnj521  28435  lshpdisj  29153  lsat0cv  29199  snatpsubN  29915  dibelval3  31313  dib1dim  31331  dvh2dim  31611  mapd0  31831  hdmap14lem13  32049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-sn 3756
  Copyright terms: Public domain W3C validator