Theorem elsn 3879

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

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

Syntax hints:   <-> wb 184   = wceq 1362   e. wcel 1755   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-sn 3866

This theorem is referenced by:  dfpr2  3880  ralsnsg  3897  rexsns  3898  rexsnsOLD  3899  disjsn  3924  snprc  3927  euabsn2  3934  snss  3987  difprsnss  3997  pwpw0  4009  eqsn  4022  snsspw  4032  pwsnALT  4074  dfnfc2  4097  uni0b  4104  uni0c  4105  sndisj  4272  reusv6OLD  4491  rext  4528  moabex  4539  exss  4543  fconstmpt  4869  opeliunxp  4877  restidsing  5150  xpdifid  5254  dmsnopg  5298  dfmpt3  5521  nfunsn  5709  dffv2  5752  fsn  5868  fnasrn  5875  fnsnb  5885  fmptsng  5887  fconstfv  5927  fvclss  5946  eusvobj2  6072  suceloni  6413  opabex3d  6544  opabex3  6545  oarec  6989  ixp0x  7279  xpsnen  7383  marypha2lem2  7674  elirrv  7800  sucprcregOLD  7803  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  dfac5lem1  8281  dfac5lem2  8282  dfac5lem4  8284  fin1a2lem11  8567  axdc4lem  8612  axcclem  8614  xrsupexmnf  11255  xrinfmexpnf  11256  iccid  11333  fzsn  11487  fzpr  11496  seqz  11838  pr2pwpr  12167  hashf1  12194  fsum2dlem  13221  incexc2  13284  ef0lem  13347  divalgmod  13593  1nprm  13751  isprm2lem  13753  vdwapun  14018  cshwsiun  14109  xpsc0  14481  xpsc1  14482  gsumvallem1  15482  symg1bas  15881  pmtrprfvalrn  15974  gex1  16070  sylow2alem1  16096  lsmdisj2  16159  0frgp  16256  0cyg  16349  prmcyg  16350  dprddisj2  16511  dprddisj2OLD  16512  ablfacrp  16541  lspdisj  17128  lidlnz  17232  psrlidm  17408  psrlidmOLD  17409  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  mulgrhm2  17769  mulgrhm2OLD  17772  ocvin  17941  maducoeval2  18288  madugsum  18291  en2top  18432  restsn  18616  ist1-3  18795  ordtt1  18825  cmpcld  18847  ptopn2  18999  snfil  19279  alexsubALTlem2  19462  alexsubALTlem3  19463  alexsubALTlem4  19464  haustsms2  19549  tsmsxplem1  19569  tsmsxplem2  19570  ust0  19636  dscopn  20008  nmoid  20163  limcdif  21193  ellimc2  21194  limcmpt  21200  limcres  21203  evlslem1  21367  ply1remlem  21519  plyeq0lem  21563  plyremlem  21655  aaliou2  21691  radcnv0  21766  abelthlem2  21782  wilthlem2  22292  vmappw  22339  ppinprm  22375  chtnprm  22377  musumsum  22417  dchrhash  22495  lgsquadlem1  22578  lgsquadlem2  22579  isusgra0  23098  nbcusgra  23194  usgrasscusgra  23214  grposn  23525  ablosn  23657  hsn0elch  24474  kerf1hrm  26145  xrge0iifiso  26219  qqhval2  26265  esumnul  26356  esumfzf  26372  sibfof  26574  plymulx0  26796  signstf0  26817  signstfvneq0  26821  sconpi1  26976  ghomsn  27154  prodsn  27320  fprod2dlem  27338  dffr5  27410  elima4  27437  wfrlem14  27584  wfrlem15  27585  brsingle  27795  dfiota3  27801  funpartfun  27821  dfrdg4  27828  0idl  28669  smprngopr  28696  isdmn3  28718  pellexlem5  29019  jm2.23  29190  flcidc  29376  funressnfv  29880  dfdfat2  29883  tz6.12-afv  29925  raldifsnb  29969  otiunsndisj  29978  otiunsndisjX  29979  rusgranumwlkb0  30417  frgrancvvdeqlem9  30480  frgrawopreglem4  30486  usg2spot2nb  30504  opeliun2xp  30565  fmptsnd  30567  snssiALTVD  31265  snssiALT  31266  bnj145OLD  31420  bnj521  31430  bj-csbsnlem  31999  lshpdisj  32205  lsat0cv  32251  snatpsubN  32967  dibelval3  34365  dib1dim  34383  dvh2dim  34663  mapd0  34883  hdmap14lem13  35101