Theorem elsni 3684

Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
elsni	⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Proof of Theorem elsni

Step	Hyp	Ref	Expression
1		elsng 3681	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 176	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  {csn 3666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-sn 3672

This theorem is referenced by:  elsn2g  3699  nelsn  3701  disjsn2  3729  sssnm  3832  disjxsn  4081  pwntru  4283  opth1  4322  elsuci  4494  ordtri2orexmid  4615  onsucsssucexmid  4619  sosng  4792  elrelimasn  5094  ressn  5269  funcnvsn  5366  funinsn  5370  funopdmsn  5823  fvconst  5831  fmptap  5833  fmptapd  5834  fvunsng  5837  mposnif  6104  1stconst  6373  2ndconst  6374  reldmtpos  6405  tpostpos  6416  1domsn  6984  ac6sfi  7068  elssdc  7075  onunsnss  7090  snon0  7113  snexxph  7128  elfi2  7150  supsnti  7183  djuf1olem  7231  eldju2ndl  7250  eldju2ndr  7251  difinfsnlem  7277  pw1m  7420  pw1on  7422  elreal2  8028  ax1rid  8075  ltxrlt  8223  un0addcl  9413  un0mulcl  9414  fzodisjsn  10392  elfzonlteqm1  10428  xnn0nnen  10671  fxnn0nninf  10673  seqf1og  10755  1exp  10802  hashinfuni  11011  hashennnuni  11013  hashprg  11043  zfz1isolemiso  11074  cats1un  11268  fisumss  11918  sumsnf  11935  fsumsplitsn  11936  fsum2dlemstep  11960  fisumcom2  11964  fprodssdc  12116  fprodunsn  12130  fprod2dlemstep  12148  fprodcom2fi  12152  fprodsplitsn  12159  divalgmod  12453  phi1  12756  dfphi2  12757  nnnn0modprm0  12793  exmidunben  13012  bassetsnn  13104  gsumress  13443  0nsg  13766  gsumfzsnfd  13897  lsssn0  14349  lspsneq0  14405  txdis1cn  14967  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycj  15450  pw0ss  15898  bj-nntrans  16369  bj-nnelirr  16371  pwtrufal  16422  sssneq  16427  exmidsbthrlem  16450