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  3831  disjxsn  4080  pwntru  4282  opth1  4321  elsuci  4493  ordtri2orexmid  4614  onsucsssucexmid  4618  sosng  4791  elrelimasn  5093  ressn  5268  funcnvsn  5365  funinsn  5369  funopdmsn  5818  fvconst  5826  fmptap  5828  fmptapd  5829  fvunsng  5832  mposnif  6097  1stconst  6365  2ndconst  6366  reldmtpos  6397  tpostpos  6408  1domsn  6974  ac6sfi  7056  onunsnss  7075  snon0  7098  snexxph  7113  elfi2  7135  supsnti  7168  djuf1olem  7216  eldju2ndl  7235  eldju2ndr  7236  difinfsnlem  7262  pw1m  7405  pw1on  7407  elreal2  8013  ax1rid  8060  ltxrlt  8208  un0addcl  9398  un0mulcl  9399  fzodisjsn  10376  elfzonlteqm1  10411  xnn0nnen  10654  fxnn0nninf  10656  seqf1og  10738  1exp  10785  hashinfuni  10994  hashennnuni  10996  hashprg  11025  zfz1isolemiso  11056  cats1un  11248  fisumss  11898  sumsnf  11915  fsumsplitsn  11916  fsum2dlemstep  11940  fisumcom2  11944  fprodssdc  12096  fprodunsn  12110  fprod2dlemstep  12128  fprodcom2fi  12132  fprodsplitsn  12139  divalgmod  12433  phi1  12736  dfphi2  12737  nnnn0modprm0  12773  exmidunben  12992  bassetsnn  13084  gsumress  13423  0nsg  13746  gsumfzsnfd  13877  lsssn0  14328  lspsneq0  14384  txdis1cn  14946  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycj  15429  pw0ss  15877  bj-nntrans  16272  bj-nnelirr  16274  pwtrufal  16322  sssneq  16327  exmidsbthrlem  16349