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

Theorem elsn 3655
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 3646 . 2  |-  { A }  =  { x  |  x  =  A }
21abeq2i 2390 1  |-  ( x  e.  { A }  <->  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684   {csn 3640
This theorem is referenced by:  dfpr2  3656  ralsns  3670  rexsns  3671  disjsn  3693  snprc  3695  euabsn2  3698  snss  3748  difprsn  3756  pwpw0  3763  eqsn  3775  snsspw  3784  pwsnALT  3822  dfnfc2  3845  uni0b  3852  uni0c  3853  sndisj  4015  rext  4222  moabex  4232  exss  4236  trsuc2OLD  4477  reusv6OLD  4545  suceloni  4604  fconstmpt  4732  opeliunxp  4740  dmsnopg  5144  dfmpt3  5366  nfunsn  5558  dffv2  5592  fsn  5696  fnasrn  5702  fconstfv  5734  fvclss  5760  opabex3  5769  eusvobj2  6337  oarec  6560  ixp0x  6844  xpsnen  6946  marypha2lem2  7189  elirrv  7311  sucprcreg  7313  cantnfp1lem1  7380  cantnfp1lem3  7382  dfac5lem1  7750  dfac5lem2  7751  dfac5lem4  7753  fin1a2lem11  8036  axdc4lem  8081  axcclem  8083  xrsupexmnf  10623  xrinfmexpnf  10624  iccid  10701  fzsn  10833  fzpr  10840  seqz  11094  hashf1  11395  fsum2dlem  12233  incexc2  12297  ef0lem  12360  divalgmod  12605  1nprm  12763  isprm2lem  12765  vdwapun  13021  xpsc0  13462  xpsc1  13463  gsumvallem1  14448  gex1  14902  sylow2alem1  14928  lsmdisj2  14991  0frgp  15088  0cyg  15179  prmcyg  15180  dprddisj2  15274  ablfacrp  15301  lspdisj  15878  lidlnz  15980  psrlidm  16148  mplcoe1  16209  mplcoe2  16211  mulgrhm2  16461  ocvin  16574  en2top  16723  restsn  16901  ist1-3  17077  ordtt1  17107  cmpcld  17129  ptopn2  17279  snfil  17559  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  haustsms2  17819  tsmsxplem1  17835  tsmsxplem2  17836  dscopn  18096  nmoid  18251  limcdif  19226  ellimc2  19227  limcmpt  19233  limcres  19236  evlslem1  19399  ply1remlem  19548  plyeq0lem  19592  plyremlem  19684  aaliou2  19720  radcnv0  19792  abelthlem2  19808  wilthlem2  20307  vmappw  20354  ppinprm  20390  chtnprm  20392  musumsum  20432  dchrhash  20510  lgsquadlem1  20593  lgsquadlem2  20594  grposn  20882  ablosn  21014  hsn0elch  21827  xrge0iifiso  23317  esumnul  23427  sconpi1  23770  ghomsn  23995  dffr5  24110  wfrlem14  24269  wfrlem15  24270  brsingle  24456  dfiota3  24462  funpartfun  24481  funpartfv  24483  dfrdg4  24488  fates  24955  restidsing  25076  pgapspf  26052  0idl  26650  smprngopr  26677  isdmn3  26699  pellexlem5  26918  jm2.23  27089  flcidc  27379  funressnfv  27991  dfdfat2  27994  tz6.12-afv  28035  isusgra0  28106  nbcusgra  28159  snssiALTVD  28602  snssiALT  28603  bnj145  28755  bnj521  28765  lshpdisj  29177  lsat0cv  29223  snatpsubN  29939  dibelval3  31337  dib1dim  31355  dvh2dim  31635  mapd0  31855  hdmap14lem13  32073
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-sn 3646
  Copyright terms: Public domain W3C validator