Theorem elsn 3998

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
elsn	|- ( x e. { A } <-> x = A )

Distinct variable group:   x, A

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		df-sn 3985	. 2 |- { A } = { x | x = A }
2	1	abeq2i 2581	1 |- ( x e. { A } <-> x = A )

Syntax hints:   <-> wb 184   = wceq 1370   e. wcel 1758   {csn 3984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-sn 3985

This theorem is referenced by:  dfpr2  3999  ralsnsg  4016  rexsns  4017  rexsnsOLD  4018  disjsn  4043  snprc  4046  euabsn2  4053  snss  4106  difprsnss  4116  pwpw0  4128  eqsn  4141  snsspw  4151  pwsnALT  4193  dfnfc2  4216  uni0b  4223  uni0c  4224  sndisj  4391  reusv6OLD  4610  rext  4647  moabex  4658  exss  4662  fconstmpt  4989  opeliunxp  4997  restidsing  5269  xpdifid  5373  dmsnopg  5417  dfmpt3  5640  nfunsn  5829  dffv2  5872  fsn  5989  fnasrn  5996  fnsnb  6006  fmptsng  6008  fconstfv  6048  fvclss  6067  eusvobj2  6192  suceloni  6533  opabex3d  6664  opabex3  6665  oarec  7110  ixp0x  7400  xpsnen  7504  marypha2lem2  7796  elirrv  7922  sucprcregOLD  7925  cantnfp1lem1  7996  cantnfp1lem3  7998  cantnfp1lem1OLD  8022  cantnfp1lem3OLD  8024  dfac5lem1  8403  dfac5lem2  8404  dfac5lem4  8406  fin1a2lem11  8689  axdc4lem  8734  axcclem  8736  xrsupexmnf  11377  xrinfmexpnf  11378  iccid  11455  fzsn  11616  fzpr  11627  seqz  11970  pr2pwpr  12300  hashf1  12327  fsum2dlem  13354  incexc2  13418  ef0lem  13481  divalgmod  13727  1nprm  13885  isprm2lem  13887  vdwapun  14152  cshwsiun  14243  xpsc0  14616  xpsc1  14617  gsumvallem1  15618  symg1bas  16019  pmtrprfvalrn  16112  gex1  16210  sylow2alem1  16236  lsmdisj2  16299  0frgp  16396  0cyg  16489  prmcyg  16490  dprddisj2  16658  dprddisj2OLD  16659  ablfacrp  16688  kerf1hrm  16953  lspdisj  17328  lidlnz  17432  psrlidm  17596  psrlidmOLD  17597  mplcoe1  17667  mplcoe5  17671  mplcoe2OLD  17673  evlslem1  17724  mulgrhm2  18051  mulgrhm2OLD  18054  ocvin  18223  maducoeval2  18577  madugsum  18580  en2top  18721  restsn  18905  ist1-3  19084  ordtt1  19114  cmpcld  19136  ptopn2  19288  snfil  19568  alexsubALTlem2  19751  alexsubALTlem3  19752  alexsubALTlem4  19753  haustsms2  19838  tsmsxplem1  19858  tsmsxplem2  19859  ust0  19925  dscopn  20297  nmoid  20452  limcdif  21483  ellimc2  21484  limcmpt  21490  limcres  21493  ply1remlem  21766  plyeq0lem  21810  plyremlem  21902  aaliou2  21938  radcnv0  22013  abelthlem2  22029  wilthlem2  22539  vmappw  22586  ppinprm  22622  chtnprm  22624  musumsum  22664  dchrhash  22742  lgsquadlem1  22825  lgsquadlem2  22826  isusgra0  23426  nbcusgra  23522  usgrasscusgra  23542  grposn  23853  ablosn  23985  hsn0elch  24802  xrge0iifiso  26509  qqhval2  26555  esumnul  26646  esumfzf  26662  sibfof  26869  plymulx0  27091  signstf0  27112  signstfvneq0  27116  sconpi1  27271  ghomsn  27450  prodsn  27616  fprod2dlem  27634  dffr5  27706  elima4  27733  wfrlem14  27880  wfrlem15  27881  brsingle  28091  dfiota3  28097  funpartfun  28117  dfrdg4  28124  0idl  28972  smprngopr  28999  isdmn3  29021  pellexlem5  29321  jm2.23  29492  flcidc  29678  funressnfv  30181  dfdfat2  30184  tz6.12-afv  30226  raldifsnb  30270  otiunsndisj  30279  otiunsndisjX  30280  rusgranumwlkb0  30718  frgrancvvdeqlem9  30781  frgrawopreglem4  30787  usg2spot2nb  30805  opeliun2xp  30867  fmptsnd  30869  snssiALTVD  31880  snssiALT  31881  bnj145OLD  32035  bnj521  32045  bj-csbsnlem  32722  lshpdisj  32955  lsat0cv  33001  snatpsubN  33717  dibelval3  35115  dib1dim  35133  dvh2dim  35413  mapd0  35633  hdmap14lem13  35851