Theorem elsn 4030

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

Syntax hints:   <-> wb 184   = wceq 1398   e. wcel 1823   {csn 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sn 4017

This theorem is referenced by:  dfpr2  4031  ralsnsg  4048  rexsns  4049  rexsnsOLD  4050  disjsn  4076  snprc  4079  euabsn2  4087  snss  4140  raldifsnb  4147  difprsnss  4151  pwpw0  4164  eqsn  4177  snsspw  4187  pwsnALT  4230  dfnfc2  4253  uni0b  4260  uni0c  4261  sndisj  4431  reusv6OLD  4648  rext  4685  moabex  4696  exss  4700  otiunsndisj  4742  fconstmpt  5032  opeliunxp  5040  restidsing  5318  xpdifid  5420  dmsnopg  5462  dfmpt3  5685  nfunsn  5879  dffv2  5921  fsn  6045  fnasrn  6053  fnsnb  6066  fmptsng  6068  fmptsnd  6069  fconstfvOLD  6109  fvclss  6129  eusvobj2  6263  suceloni  6621  opabex3d  6751  opabex3  6752  oarec  7203  ixp0x  7490  xpsnen  7594  marypha2lem2  7888  elirrv  8015  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  dfac5lem1  8495  dfac5lem2  8496  dfac5lem4  8498  fin1a2lem11  8781  axdc4lem  8826  axcclem  8828  xrsupexmnf  11499  xrinfmexpnf  11500  iccid  11577  fzsn  11729  fzpr  11739  seqz  12137  hashf1  12490  pr2pwpr  12504  fsum2dlem  13667  incexc2  13732  prodsn  13849  fprod2dlem  13866  ef0lem  13896  divalgmod  14148  1nprm  14306  isprm2lem  14308  vdwapun  14576  cshwsiun  14668  xpsc0  15049  xpsc1  15050  mgmidsssn0  16095  mnd1id  16162  symg1bas  16620  pmtrprfvalrn  16712  gex1  16810  sylow2alem1  16836  lsmdisj2  16899  0frgp  16996  0cyg  17094  prmcyg  17095  dprddisj2  17282  dprddisj2OLD  17283  ablfacrp  17312  kerf1hrm  17587  lspdisj  17966  lidlnz  18071  psrlidm  18251  psrlidmOLD  18252  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  evlslem1  18379  mulgrhm2  18711  ocvin  18878  maducoeval2  19309  madugsum  19312  en2top  19654  restsn  19838  ist1-3  20017  ordtt1  20047  cmpcld  20069  unisngl  20194  dissnlocfin  20196  ptopn2  20251  snfil  20531  alexsubALTlem2  20714  alexsubALTlem3  20715  alexsubALTlem4  20716  haustsms2  20801  tsmsxplem1  20821  tsmsxplem2  20822  ust0  20888  dscopn  21260  nmoid  21415  limcdif  22446  ellimc2  22447  limcmpt  22453  limcres  22456  ply1remlem  22729  plyeq0lem  22773  plyremlem  22866  aaliou2  22902  radcnv0  22977  abelthlem2  22993  wilthlem2  23541  vmappw  23588  ppinprm  23624  chtnprm  23626  musumsum  23666  dchrhash  23744  lgsquadlem1  23827  lgsquadlem2  23828  isusgra0  24549  usgraop  24552  nbcusgra  24665  usgrasscusgra  24685  rusgranumwlkb0  25155  frgrancvvdeqlem9  25243  frgrawopreglem4  25249  usg2spot2nb  25267  grposn  25415  ablosn  25547  hsn0elch  26364  iunxsngf  27634  elsnxp  27684  xrge0iifiso  28152  qqhval2  28197  esumnul  28277  esumrnmpt2  28297  esumfzf  28298  sibfof  28546  plymulx0  28768  signstf0  28789  signstfvneq0  28793  sconpi1  28948  ghomsn  29292  dffr5  29423  elima4  29449  wfrlem14  29596  wfrlem15  29597  brsingle  29795  dfiota3  29801  funpartfun  29821  dfrdg4  29828  0idl  30662  smprngopr  30689  isdmn3  30711  pellexlem5  31008  jm2.23  31177  flcidc  31364  iccintsng  31802  icoiccdif  31803  prodsnf  31826  limcrecl  31874  lptioo2  31876  lptioo1  31877  limcresiooub  31887  limcresioolb  31888  icccncfext  31929  dvmptfprodlem  31980  dvnprodlem3  31984  dirkercncflem2  32125  fourierdlem40  32168  fourierdlem48  32176  fourierdlem51  32179  fourierdlem62  32190  fourierdlem66  32194  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem78  32206  fourierdlem79  32207  fourierdlem93  32221  fourierdlem101  32229  fourierdlem103  32231  fourierdlem104  32232  fouriersw  32253  elaa2  32256  etransclem44  32300  etransc  32305  funressnfv  32452  dfdfat2  32455  tz6.12-afv  32497  otiunsndisjX  32675  xpsnopab  32825  opeliun2xp  33176  aacllem  33604  snssiALTVD  34027  snssiALT  34028  bnj145OLD  34183  bnj521  34193  bj-csbsnlem  34871  lshpdisj  35109  lsat0cv  35155  snatpsubN  35871  dibelval3  37271  dib1dim  37289  dvh2dim  37569  mapd0  37789  hdmap14lem13  38007  snhesn  38259