Theorem elsn 4041

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

Syntax hints:   <-> wb 184   = wceq 1379   e. wcel 1767   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sn 4028

This theorem is referenced by:  dfpr2  4042  ralsnsg  4059  rexsns  4060  rexsnsOLD  4061  disjsn  4088  snprc  4091  euabsn2  4098  snss  4151  raldifsnb  4158  difprsnss  4162  pwpw0  4175  eqsn  4188  snsspw  4198  pwsnALT  4240  dfnfc2  4263  uni0b  4270  uni0c  4271  sndisj  4439  reusv6OLD  4658  rext  4695  moabex  4706  exss  4710  otiunsndisj  4753  fconstmpt  5043  opeliunxp  5051  restidsing  5330  xpdifid  5435  dmsnopg  5479  dfmpt3  5703  nfunsn  5897  dffv2  5940  fsn  6059  fnasrn  6067  fnsnb  6080  fmptsng  6082  fmptsnd  6083  fconstfv  6123  fvclss  6142  eusvobj2  6277  suceloni  6632  opabex3d  6762  opabex3  6763  oarec  7211  ixp0x  7497  xpsnen  7601  marypha2lem2  7896  elirrv  8023  sucprcregOLD  8026  cantnfp1lem1  8097  cantnfp1lem3  8099  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  dfac5lem1  8504  dfac5lem2  8505  dfac5lem4  8507  fin1a2lem11  8790  axdc4lem  8835  axcclem  8837  xrsupexmnf  11496  xrinfmexpnf  11497  iccid  11574  fzsn  11725  fzpr  11735  seqz  12123  hashf1  12472  pr2pwpr  12486  fsum2dlem  13548  incexc2  13613  ef0lem  13676  divalgmod  13923  1nprm  14081  isprm2lem  14083  vdwapun  14351  cshwsiun  14442  xpsc0  14815  xpsc1  14816  mnd1id  15781  gsumvallem1  15822  symg1bas  16226  pmtrprfvalrn  16319  gex1  16417  sylow2alem1  16443  lsmdisj2  16506  0frgp  16603  0cyg  16698  prmcyg  16699  dprddisj2  16889  dprddisj2OLD  16890  ablfacrp  16919  kerf1hrm  17192  lspdisj  17571  lidlnz  17675  psrlidm  17855  psrlidmOLD  17856  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  evlslem1  17983  mulgrhm2  18328  mulgrhm2OLD  18331  ocvin  18500  maducoeval2  18937  madugsum  18940  en2top  19281  restsn  19465  ist1-3  19644  ordtt1  19674  cmpcld  19696  ptopn2  19848  snfil  20128  alexsubALTlem2  20311  alexsubALTlem3  20312  alexsubALTlem4  20313  haustsms2  20398  tsmsxplem1  20418  tsmsxplem2  20419  ust0  20485  dscopn  20857  nmoid  21012  limcdif  22043  ellimc2  22044  limcmpt  22050  limcres  22053  ply1remlem  22326  plyeq0lem  22370  plyremlem  22462  aaliou2  22498  radcnv0  22573  abelthlem2  22589  wilthlem2  23099  vmappw  23146  ppinprm  23182  chtnprm  23184  musumsum  23224  dchrhash  23302  lgsquadlem1  23385  lgsquadlem2  23386  isusgra0  24051  usgraop  24054  nbcusgra  24167  usgrasscusgra  24187  rusgranumwlkb0  24657  frgrancvvdeqlem9  24746  frgrawopreglem4  24752  usg2spot2nb  24770  grposn  24921  ablosn  25053  hsn0elch  25870  xrge0iifiso  27581  qqhval2  27627  esumnul  27727  esumfzf  27743  sibfof  27950  plymulx0  28172  signstf0  28193  signstfvneq0  28197  sconpi1  28352  ghomsn  28531  prodsn  28697  fprod2dlem  28715  dffr5  28787  elima4  28814  wfrlem14  28961  wfrlem15  28962  brsingle  29172  dfiota3  29178  funpartfun  29198  dfrdg4  29205  0idl  30053  smprngopr  30080  isdmn3  30102  pellexlem5  30401  jm2.23  30570  flcidc  30756  iccintsng  31155  icoiccdif  31156  limcrecl  31199  lptioo2  31201  lptioo1  31202  limcresiooub  31212  limcresioolb  31213  icccncfext  31254  dirkercncflem1  31431  dirkercncflem2  31432  fourierdlem40  31475  fourierdlem48  31483  fourierdlem51  31486  fourierdlem62  31497  fourierdlem66  31501  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem78  31513  fourierdlem79  31514  fourierdlem93  31528  fourierdlem101  31536  fourierdlem103  31538  fourierdlem104  31539  fouriersw  31560  funressnfv  31708  dfdfat2  31711  tz6.12-afv  31753  otiunsndisjX  31796  opeliun2xp  32018  snssiALTVD  32725  snssiALT  32726  bnj145OLD  32880  bnj521  32890  bj-csbsnlem  33569  lshpdisj  33802  lsat0cv  33848  snatpsubN  34564  dibelval3  35962  dib1dim  35980  dvh2dim  36260  mapd0  36480  hdmap14lem13  36698