Theorem elsn 3982

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

Syntax hints:   <-> wb 188   = wceq 1444   e. wcel 1887   {csn 3968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-12 1933  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-sn 3969

This theorem is referenced by:  dfpr2  3983  ralsnsg  4003  rexsns  4004  rexsnsOLD  4005  disjsn  4032  snprc  4035  euabsn2  4043  snss  4096  raldifsnb  4103  difprsnss  4107  pwpw0  4120  eqsn  4133  snsspw  4143  pwsnALT  4193  dfnfc2  4216  uni0b  4223  uni0c  4224  sndisj  4394  rext  4648  moabex  4659  exss  4663  otiunsndisj  4707  fconstmpt  4878  opeliunxp  4886  restidsing  5161  xpdifid  5265  dmsnopg  5307  elsnxp  5378  dfmpt3  5698  nfunsn  5896  dffv2  5938  fsn  6061  fnasrn  6070  fnsnb  6083  fmptsng  6085  fmptsnd  6086  fconstfvOLD  6127  fvclss  6147  eusvobj2  6283  suceloni  6640  opabex3d  6771  opabex3  6772  wfrlem14  7049  wfrlem15  7050  oarec  7263  ixp0x  7550  xpsnen  7656  marypha2lem2  7950  elirrv  8112  cantnfp1lem1  8183  cantnfp1lem3  8185  dfac5lem1  8554  dfac5lem2  8555  dfac5lem4  8557  fin1a2lem11  8840  axdc4lem  8885  axcclem  8887  xrsupexmnf  11590  xrinfmexpnf  11591  iccid  11681  fzsn  11840  fzpr  11851  seqz  12261  hashf1  12620  pr2pwpr  12636  fsum2dlem  13831  incexc2  13896  prodsn  14016  prodsnf  14018  fprod2dlem  14034  ef0lem  14133  divalgmod  14387  lcmfunsnlem2  14613  1nprm  14629  isprm2lem  14631  vdwapun  14924  prmodvdslcmf  15005  prmordvdslcmfOLD  15019  prmordvdslcmsOLDOLD  15021  cshwsiun  15070  xpsc0  15466  xpsc1  15467  mgmidsssn0  16512  mnd1id  16579  symg1bas  17037  pmtrprfvalrn  17129  gex1  17243  sylow2alem1  17269  lsmdisj2  17332  0frgp  17429  0cyg  17527  prmcyg  17528  dprddisj2  17672  ablfacrp  17699  kerf1hrm  17971  lspdisj  18348  lidlnz  18452  psrlidm  18627  mplcoe1  18689  mplcoe5  18692  evlslem1  18738  mulgrhm2  19070  ocvin  19237  maducoeval2  19665  madugsum  19668  en2top  20001  restsn  20186  ist1-3  20365  ordtt1  20395  cmpcld  20417  unisngl  20542  dissnlocfin  20544  ptopn2  20599  snfil  20879  alexsubALTlem2  21063  alexsubALTlem3  21064  alexsubALTlem4  21065  haustsms2  21151  tsmsxplem1  21167  tsmsxplem2  21168  ust0  21234  dscopn  21588  nmoid  21763  limcdif  22831  ellimc2  22832  limcmpt  22838  limcres  22841  ply1remlem  23113  plyeq0lem  23164  plyremlem  23257  aaliou2  23296  radcnv0  23371  abelthlem2  23387  wilthlem2  23994  vmappw  24043  ppinprm  24079  chtnprm  24081  musumsum  24121  dchrhash  24199  lgsquadlem1  24282  lgsquadlem2  24283  isusgra0  25074  usgraop  25077  nbcusgra  25191  usgrasscusgra  25211  rusgranumwlkb0  25681  frgrancvvdeqlem9  25769  frgrawopreglem4  25775  usg2spot2nb  25793  grposn  25943  ablosn  26075  hsn0elch  26901  iunxsngf  28172  xrge0iifiso  28741  qqhval2  28786  esumnul  28869  esumrnmpt2  28889  esumfzf  28890  sibfof  29173  plymulx0  29436  signstf0  29457  signstfvneq0  29461  bnj145OLD  29535  bnj521  29545  sconpi1  29962  ghomsn  30306  dffr5  30393  elima4  30421  brsingle  30684  dfiota3  30690  funpartfun  30710  dfrdg4  30718  fwddifn0  30931  bj-csbsnlem  31505  mptsnunlem  31740  poimirlem23  31963  poimirlem26  31966  poimirlem27  31967  0idl  32258  smprngopr  32285  isdmn3  32307  lshpdisj  32553  lsat0cv  32599  snatpsubN  33315  dibelval3  34715  dib1dim  34733  dvh2dim  35013  mapd0  35233  hdmap14lem13  35451  pellexlem5  35677  jm2.23  35851  flcidc  36040  snhesn  36382  snssiALTVD  37223  snssiALT  37224  iccintsng  37624  icoiccdif  37625  limcrecl  37709  lptioo2  37711  lptioo1  37712  limcresiooub  37723  limcresioolb  37724  icccncfext  37765  dvmptfprodlem  37819  dvnprodlem3  37823  dirkercncflem2  37966  fourierdlem40  38010  fourierdlem48  38018  fourierdlem51  38021  fourierdlem62  38032  fourierdlem66  38036  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem78  38048  fourierdlem79  38049  fourierdlem93  38063  fourierdlem101  38071  fourierdlem103  38073  fourierdlem104  38074  fouriersw  38095  elaa2  38099  etransclem44  38143  sge00  38218  funressnfv  38629  dfdfat2  38633  tz6.12-afv  38675  iccpartgtl  38740  iccpartgt  38741  iccpartleu  38742  iccpartgel  38743  nnsum4primeseven  38895  nnsum4primesevenALTV  38896  bgoldbtbnd  38904  otiunsndisjX  39006  fundmge2nop  39026  cplgr1v  39497  xpsnopab  39818  opeliun2xp  40167  aacllem  40593