Theorem elsn 3973

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 3960	. 2 |- { A } = { x | x = A }
2	1	abeq2i 2583	1 |- ( x e. { A } <-> x = A )

Syntax hints:   <-> wb 189   = wceq 1452   e. wcel 1904   {csn 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-sn 3960

This theorem is referenced by:  dfpr2  3974  ralsnsg  3995  rexsns  3996  disjsn  4023  snprc  4027  euabsn2  4034  snss  4087  raldifsnb  4094  difprsnss  4098  pwpw0  4111  eqsn  4125  snsspw  4135  pwsnALT  4185  dfnfc2  4208  uni0b  4215  uni0c  4216  sndisj  4387  rext  4648  moabex  4659  exss  4663  otiunsndisj  4707  fconstmpt  4883  opeliunxp  4891  restidsing  5167  xpdifid  5271  dmsnopg  5314  elsnxp  5385  dfmpt3  5708  nfunsn  5910  dffv2  5953  fsn  6077  fnasrn  6086  fnsnb  6099  fmptsng  6101  fmptsnd  6102  fvclss  6165  eusvobj2  6301  suceloni  6659  opabex3d  6790  opabex3  6791  wfrlem14  7067  wfrlem15  7068  oarec  7281  ixp0x  7568  xpsnen  7674  marypha2lem2  7968  elirrv  8130  cantnfp1lem1  8201  cantnfp1lem3  8203  dfac5lem1  8572  dfac5lem2  8573  dfac5lem4  8575  fin1a2lem11  8858  axdc4lem  8903  axcclem  8905  xrsupexmnf  11615  xrinfmexpnf  11616  iccid  11706  fzsn  11866  fzpr  11877  seqz  12299  hashf1  12661  pr2pwpr  12677  fsum2dlem  13908  incexc2  13973  prodsn  14093  prodsnf  14095  fprod2dlem  14111  ef0lem  14210  divalgmod  14466  lcmfunsnlem2  14692  1nprm  14708  isprm2lem  14710  vdwapun  15003  prmodvdslcmf  15084  prmordvdslcmfOLD  15098  prmordvdslcmsOLDOLD  15100  cshwsiun  15148  xpsc0  15544  xpsc1  15545  mgmidsssn0  16590  mnd1id  16657  symg1bas  17115  pmtrprfvalrn  17207  gex1  17321  sylow2alem1  17347  lsmdisj2  17410  0frgp  17507  0cyg  17605  prmcyg  17606  dprddisj2  17750  ablfacrp  17777  kerf1hrm  18049  lspdisj  18426  lidlnz  18529  psrlidm  18704  mplcoe1  18766  mplcoe5  18769  evlslem1  18815  mulgrhm2  19147  ocvin  19314  maducoeval2  19742  madugsum  19745  en2top  20078  restsn  20263  ist1-3  20442  ordtt1  20472  cmpcld  20494  unisngl  20619  dissnlocfin  20621  ptopn2  20676  snfil  20957  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALTlem4  21143  haustsms2  21229  tsmsxplem1  21245  tsmsxplem2  21246  ust0  21312  dscopn  21666  nmoid  21841  limcdif  22910  ellimc2  22911  limcmpt  22917  limcres  22920  ply1remlem  23192  plyeq0lem  23243  plyremlem  23336  aaliou2  23375  radcnv0  23450  abelthlem2  23466  wilthlem2  24073  vmappw  24122  ppinprm  24158  chtnprm  24160  musumsum  24200  dchrhash  24278  lgsquadlem1  24361  lgsquadlem2  24362  isusgra0  25153  usgraop  25156  nbcusgra  25270  usgrasscusgra  25290  rusgranumwlkb0  25760  frgrancvvdeqlem9  25848  frgrawopreglem4  25854  usg2spot2nb  25872  grposn  26024  ablosn  26156  hsn0elch  26982  iunxsngf  28250  xrge0iifiso  28815  qqhval2  28860  esumnul  28943  esumrnmpt2  28963  esumfzf  28964  sibfof  29246  plymulx0  29508  signstf0  29529  signstfvneq0  29533  bnj145OLD  29607  bnj521  29617  sconpi1  30034  ghomsn  30378  dffr5  30464  elima4  30492  brsingle  30755  dfiota3  30761  funpartfun  30781  dfrdg4  30789  fwddifn0  31002  bj-csbsnlem  31573  mptsnunlem  31810  poimirlem23  32027  poimirlem26  32030  poimirlem27  32031  0idl  32322  smprngopr  32349  isdmn3  32371  lshpdisj  32624  lsat0cv  32670  snatpsubN  33386  dibelval3  34786  dib1dim  34804  dvh2dim  35084  mapd0  35304  hdmap14lem13  35522  pellexlem5  35748  jm2.23  35922  flcidc  36111  snhesn  36453  snssiALTVD  37286  snssiALT  37287  fsneq  37558  iccintsng  37720  icoiccdif  37721  limcrecl  37806  lptioo2  37808  lptioo1  37809  limcresiooub  37820  limcresioolb  37821  icccncfext  37862  dvmptfprodlem  37916  dvnprodlem3  37920  dirkercncflem2  38078  fourierdlem40  38122  fourierdlem48  38130  fourierdlem51  38133  fourierdlem62  38144  fourierdlem66  38148  fourierdlem74  38156  fourierdlem75  38157  fourierdlem76  38158  fourierdlem78  38160  fourierdlem79  38161  fourierdlem93  38175  fourierdlem101  38183  fourierdlem103  38185  fourierdlem104  38186  fouriersw  38207  elaa2  38211  etransclem44  38255  sge00  38332  funressnfv  38774  dfdfat2  38778  tz6.12-afv  38820  iccpartgtl  38885  iccpartgt  38886  iccpartleu  38887  iccpartgel  38888  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  bgoldbtbnd  39049  otiunsndisjX  39152  fundmge2nop  39172  cplgr1v  39662  xpsnopab  40273  opeliun2xp  40622  aacllem  41046