Theorem elsn 4011

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

Syntax hints:   <-> wb 188   = wceq 1438   e. wcel 1869   {csn 3997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-12 1906  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-sn 3998

This theorem is referenced by:  dfpr2  4012  ralsnsg  4029  rexsns  4030  rexsnsOLD  4031  disjsn  4058  snprc  4061  euabsn2  4069  snss  4122  raldifsnb  4129  difprsnss  4133  pwpw0  4146  eqsn  4159  snsspw  4169  pwsnALT  4212  dfnfc2  4235  uni0b  4242  uni0c  4243  sndisj  4413  rext  4667  moabex  4678  exss  4682  otiunsndisj  4724  fconstmpt  4895  opeliunxp  4903  restidsing  5178  xpdifid  5282  dmsnopg  5324  elsnxp  5395  dfmpt3  5714  nfunsn  5910  dffv2  5952  fsn  6074  fnasrn  6083  fnsnb  6096  fmptsng  6098  fmptsnd  6099  fconstfvOLD  6140  fvclss  6160  eusvobj2  6296  suceloni  6652  opabex3d  6783  opabex3  6784  wfrlem14  7055  wfrlem15  7056  oarec  7269  ixp0x  7556  xpsnen  7660  marypha2lem2  7954  elirrv  8116  cantnfp1lem1  8186  cantnfp1lem3  8188  dfac5lem1  8556  dfac5lem2  8557  dfac5lem4  8559  fin1a2lem11  8842  axdc4lem  8887  axcclem  8889  xrsupexmnf  11592  xrinfmexpnf  11593  iccid  11683  fzsn  11842  fzpr  11853  seqz  12262  hashf1  12619  pr2pwpr  12634  fsum2dlem  13824  incexc2  13889  prodsn  14009  prodsnf  14011  fprod2dlem  14027  ef0lem  14126  divalgmod  14380  lcmfunsnlem2  14606  1nprm  14622  isprm2lem  14624  vdwapun  14917  prmodvdslcmf  14998  prmordvdslcmfOLD  15012  prmordvdslcmsOLDOLD  15014  cshwsiun  15063  xpsc0  15459  xpsc1  15460  mgmidsssn0  16505  mnd1id  16572  symg1bas  17030  pmtrprfvalrn  17122  gex1  17236  sylow2alem1  17262  lsmdisj2  17325  0frgp  17422  0cyg  17520  prmcyg  17521  dprddisj2  17665  ablfacrp  17692  kerf1hrm  17964  lspdisj  18341  lidlnz  18445  psrlidm  18620  mplcoe1  18682  mplcoe5  18685  evlslem1  18731  mulgrhm2  19062  ocvin  19229  maducoeval2  19657  madugsum  19660  en2top  19993  restsn  20178  ist1-3  20357  ordtt1  20387  cmpcld  20409  unisngl  20534  dissnlocfin  20536  ptopn2  20591  snfil  20871  alexsubALTlem2  21055  alexsubALTlem3  21056  alexsubALTlem4  21057  haustsms2  21143  tsmsxplem1  21159  tsmsxplem2  21160  ust0  21226  dscopn  21580  nmoid  21755  limcdif  22823  ellimc2  22824  limcmpt  22830  limcres  22833  ply1remlem  23105  plyeq0lem  23156  plyremlem  23249  aaliou2  23288  radcnv0  23363  abelthlem2  23379  wilthlem2  23986  vmappw  24035  ppinprm  24071  chtnprm  24073  musumsum  24113  dchrhash  24191  lgsquadlem1  24274  lgsquadlem2  24275  isusgra0  25066  usgraop  25069  nbcusgra  25183  usgrasscusgra  25203  rusgranumwlkb0  25673  frgrancvvdeqlem9  25761  frgrawopreglem4  25767  usg2spot2nb  25785  grposn  25935  ablosn  26067  hsn0elch  26893  iunxsngf  28168  xrge0iifiso  28743  qqhval2  28788  esumnul  28871  esumrnmpt2  28891  esumfzf  28892  sibfof  29175  plymulx0  29438  signstf0  29459  signstfvneq0  29463  bnj145OLD  29537  bnj521  29547  sconpi1  29964  ghomsn  30308  dffr5  30394  elima4  30422  brsingle  30683  dfiota3  30689  funpartfun  30709  dfrdg4  30717  fwddifn0  30930  bj-csbsnlem  31468  mptsnunlem  31687  poimirlem23  31883  poimirlem26  31886  poimirlem27  31887  0idl  32178  smprngopr  32205  isdmn3  32227  lshpdisj  32478  lsat0cv  32524  snatpsubN  33240  dibelval3  34640  dib1dim  34658  dvh2dim  34938  mapd0  35158  hdmap14lem13  35376  pellexlem5  35603  jm2.23  35777  flcidc  35966  snhesn  36246  snssiALTVD  37090  snssiALT  37091  iccintsng  37461  icoiccdif  37462  limcrecl  37535  lptioo2  37537  lptioo1  37538  limcresiooub  37549  limcresioolb  37550  icccncfext  37591  dvmptfprodlem  37645  dvnprodlem3  37649  dirkercncflem2  37792  fourierdlem40  37836  fourierdlem48  37844  fourierdlem51  37847  fourierdlem62  37858  fourierdlem66  37862  fourierdlem74  37870  fourierdlem75  37871  fourierdlem76  37872  fourierdlem78  37874  fourierdlem79  37875  fourierdlem93  37889  fourierdlem101  37897  fourierdlem103  37899  fourierdlem104  37900  fouriersw  37921  elaa2  37925  etransclem44  37969  sge00  38012  funressnfv  38348  dfdfat2  38351  tz6.12-afv  38393  iccpartgtl  38458  iccpartgt  38459  iccpartleu  38460  iccpartgel  38461  nnsum4primeseven  38613  nnsum4primesevenALTV  38614  bgoldbtbnd  38622  otiunsndisjX  38714  fundmge2nop  38730  isusgr0  38878  ausgrumgri  38888  xpsnopab  39069  opeliun2xp  39420  aacllem  39846