Theorem elsn 3886

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

Syntax hints:   <-> wb 184   = wceq 1369   e. wcel 1756   {csn 3872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-sn 3873

This theorem is referenced by:  dfpr2  3887  ralsnsg  3904  rexsns  3905  rexsnsOLD  3906  disjsn  3931  snprc  3934  euabsn2  3941  snss  3994  difprsnss  4004  pwpw0  4016  eqsn  4029  snsspw  4039  pwsnALT  4081  dfnfc2  4104  uni0b  4111  uni0c  4112  sndisj  4279  reusv6OLD  4498  rext  4535  moabex  4546  exss  4550  fconstmpt  4877  opeliunxp  4885  restidsing  5157  xpdifid  5261  dmsnopg  5305  dfmpt3  5528  nfunsn  5716  dffv2  5759  fsn  5876  fnasrn  5883  fnsnb  5893  fmptsng  5895  fconstfv  5935  fvclss  5954  eusvobj2  6079  suceloni  6419  opabex3d  6550  opabex3  6551  oarec  6993  ixp0x  7283  xpsnen  7387  marypha2lem2  7678  elirrv  7804  sucprcregOLD  7807  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  dfac5lem1  8285  dfac5lem2  8286  dfac5lem4  8288  fin1a2lem11  8571  axdc4lem  8616  axcclem  8618  xrsupexmnf  11259  xrinfmexpnf  11260  iccid  11337  fzsn  11492  fzpr  11503  seqz  11846  pr2pwpr  12175  hashf1  12202  fsum2dlem  13229  incexc2  13293  ef0lem  13356  divalgmod  13602  1nprm  13760  isprm2lem  13762  vdwapun  14027  cshwsiun  14118  xpsc0  14490  xpsc1  14491  gsumvallem1  15491  symg1bas  15892  pmtrprfvalrn  15985  gex1  16081  sylow2alem1  16107  lsmdisj2  16170  0frgp  16267  0cyg  16360  prmcyg  16361  dprddisj2  16527  dprddisj2OLD  16528  ablfacrp  16557  lspdisj  17186  lidlnz  17290  psrlidm  17454  psrlidmOLD  17455  mplcoe1  17524  mplcoe5  17528  mplcoe2OLD  17530  evlslem1  17581  mulgrhm2  17907  mulgrhm2OLD  17910  ocvin  18079  maducoeval2  18426  madugsum  18429  en2top  18570  restsn  18754  ist1-3  18933  ordtt1  18963  cmpcld  18985  ptopn2  19137  snfil  19417  alexsubALTlem2  19600  alexsubALTlem3  19601  alexsubALTlem4  19602  haustsms2  19687  tsmsxplem1  19707  tsmsxplem2  19708  ust0  19774  dscopn  20146  nmoid  20301  limcdif  21331  ellimc2  21332  limcmpt  21338  limcres  21341  ply1remlem  21614  plyeq0lem  21658  plyremlem  21750  aaliou2  21786  radcnv0  21861  abelthlem2  21877  wilthlem2  22387  vmappw  22434  ppinprm  22470  chtnprm  22472  musumsum  22512  dchrhash  22590  lgsquadlem1  22673  lgsquadlem2  22674  isusgra0  23243  nbcusgra  23339  usgrasscusgra  23359  grposn  23670  ablosn  23802  hsn0elch  24619  kerf1hrm  26260  xrge0iifiso  26334  qqhval2  26380  esumnul  26471  esumfzf  26487  sibfof  26695  plymulx0  26917  signstf0  26938  signstfvneq0  26942  sconpi1  27097  ghomsn  27276  prodsn  27442  fprod2dlem  27460  dffr5  27532  elima4  27559  wfrlem14  27706  wfrlem15  27707  brsingle  27917  dfiota3  27923  funpartfun  27943  dfrdg4  27950  0idl  28796  smprngopr  28823  isdmn3  28845  pellexlem5  29145  jm2.23  29316  flcidc  29502  funressnfv  30005  dfdfat2  30008  tz6.12-afv  30050  raldifsnb  30094  otiunsndisj  30103  otiunsndisjX  30104  rusgranumwlkb0  30542  frgrancvvdeqlem9  30605  frgrawopreglem4  30611  usg2spot2nb  30629  opeliun2xp  30690  fmptsnd  30692  snssiALTVD  31492  snssiALT  31493  bnj145OLD  31647  bnj521  31657  bj-csbsnlem  32305  lshpdisj  32525  lsat0cv  32571  snatpsubN  33287  dibelval3  34685  dib1dim  34703  dvh2dim  34983  mapd0  35203  hdmap14lem13  35421