Theorem elsn 4024

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

Syntax hints:   <-> wb 184   = wceq 1381   e. wcel 1802   {csn 4010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-12 1838  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-sn 4011

This theorem is referenced by:  dfpr2  4025  ralsnsg  4042  rexsns  4043  rexsnsOLD  4044  disjsn  4071  snprc  4074  euabsn2  4082  snss  4135  raldifsnb  4142  difprsnss  4146  pwpw0  4159  eqsn  4172  snsspw  4182  pwsnALT  4225  dfnfc2  4248  uni0b  4255  uni0c  4256  sndisj  4425  reusv6OLD  4644  rext  4681  moabex  4692  exss  4696  otiunsndisj  4739  fconstmpt  5029  opeliunxp  5037  restidsing  5316  xpdifid  5421  dmsnopg  5465  dfmpt3  5689  nfunsn  5883  dffv2  5927  fsn  6050  fnasrn  6058  fnsnb  6071  fmptsng  6073  fmptsnd  6074  fconstfvOLD  6114  fvclss  6135  eusvobj2  6270  suceloni  6629  opabex3d  6759  opabex3  6760  oarec  7209  ixp0x  7495  xpsnen  7599  marypha2lem2  7894  elirrv  8021  sucprcregOLD  8024  cantnfp1lem1  8095  cantnfp1lem3  8097  cantnfp1lem1OLD  8121  cantnfp1lem3OLD  8123  dfac5lem1  8502  dfac5lem2  8503  dfac5lem4  8505  fin1a2lem11  8788  axdc4lem  8833  axcclem  8835  xrsupexmnf  11500  xrinfmexpnf  11501  iccid  11578  fzsn  11729  fzpr  11739  seqz  12129  hashf1  12480  pr2pwpr  12494  fsum2dlem  13559  incexc2  13624  ef0lem  13687  divalgmod  13936  1nprm  14094  isprm2lem  14096  vdwapun  14364  cshwsiun  14456  xpsc0  14829  xpsc1  14830  mgmidsssn0  15765  mnd1id  15832  symg1bas  16290  pmtrprfvalrn  16382  gex1  16480  sylow2alem1  16506  lsmdisj2  16569  0frgp  16666  0cyg  16764  prmcyg  16765  dprddisj2  16955  dprddisj2OLD  16956  ablfacrp  16985  kerf1hrm  17260  lspdisj  17639  lidlnz  17744  psrlidm  17924  psrlidmOLD  17925  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  evlslem1  18052  mulgrhm2  18400  mulgrhm2OLD  18403  ocvin  18572  maducoeval2  19009  madugsum  19012  en2top  19353  restsn  19537  ist1-3  19716  ordtt1  19746  cmpcld  19768  unisngl  19894  dissnlocfin  19896  ptopn2  19951  snfil  20231  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  haustsms2  20501  tsmsxplem1  20521  tsmsxplem2  20522  ust0  20588  dscopn  20960  nmoid  21115  limcdif  22146  ellimc2  22147  limcmpt  22153  limcres  22156  ply1remlem  22429  plyeq0lem  22473  plyremlem  22565  aaliou2  22601  radcnv0  22676  abelthlem2  22692  wilthlem2  23208  vmappw  23255  ppinprm  23291  chtnprm  23293  musumsum  23333  dchrhash  23411  lgsquadlem1  23494  lgsquadlem2  23495  isusgra0  24212  usgraop  24215  nbcusgra  24328  usgrasscusgra  24348  rusgranumwlkb0  24818  frgrancvvdeqlem9  24906  frgrawopreglem4  24912  usg2spot2nb  24930  grposn  25082  ablosn  25214  hsn0elch  26031  xrge0iifiso  27783  qqhval2  27829  esumnul  27925  esumfzf  27941  sibfof  28148  plymulx0  28370  signstf0  28391  signstfvneq0  28395  sconpi1  28550  ghomsn  28894  prodsn  29060  fprod2dlem  29078  dffr5  29150  elima4  29177  wfrlem14  29324  wfrlem15  29325  brsingle  29535  dfiota3  29541  funpartfun  29561  dfrdg4  29568  0idl  30390  smprngopr  30417  isdmn3  30439  pellexlem5  30737  jm2.23  30906  flcidc  31092  iccintsng  31495  icoiccdif  31496  limcrecl  31539  lptioo2  31541  lptioo1  31542  limcresiooub  31552  limcresioolb  31553  icccncfext  31593  dirkercncflem2  31771  fourierdlem40  31814  fourierdlem48  31822  fourierdlem51  31825  fourierdlem62  31836  fourierdlem66  31840  fourierdlem74  31848  fourierdlem75  31849  fourierdlem76  31850  fourierdlem78  31852  fourierdlem79  31853  fourierdlem93  31867  fourierdlem101  31875  fourierdlem103  31877  fourierdlem104  31878  fouriersw  31899  funressnfv  32047  dfdfat2  32050  tz6.12-afv  32092  otiunsndisjX  32135  xpsnopab  32287  opeliun2xp  32630  snssiALTVD  33335  snssiALT  33336  bnj145OLD  33490  bnj521  33500  bj-csbsnlem  34182  lshpdisj  34414  lsat0cv  34460  snatpsubN  35176  dibelval3  36576  dib1dim  36594  dvh2dim  36874  mapd0  37094  hdmap14lem13  37312