Theorem elsni 3687

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 3684	. 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
2	1	ibi 176	1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  elsn2g  3702  nelsn  3704  disjsn2  3732  rabsnifsb  3737  rabsnif  3738  sssnm  3837  disjxsn  4086  pwntru  4289  opth1  4328  elsuci  4500  ordtri2orexmid  4621  onsucsssucexmid  4625  sosng  4799  elrelimasn  5102  ressn  5277  funcnvsn  5375  funinsn  5379  funopdmsn  5834  fvconst  5842  fmptap  5844  fmptapd  5845  fvunsng  5848  mposnif  6115  1stconst  6386  2ndconst  6387  reldmtpos  6419  tpostpos  6430  1domsn  7001  ac6sfi  7087  elssdc  7094  onunsnss  7109  snon0  7134  snexxph  7149  elfi2  7171  supsnti  7204  djuf1olem  7252  eldju2ndl  7271  eldju2ndr  7272  difinfsnlem  7298  pw1m  7442  pw1on  7444  elreal2  8050  ax1rid  8097  ltxrlt  8245  un0addcl  9435  un0mulcl  9436  fzodisjsn  10419  elfzonlteqm1  10456  xnn0nnen  10700  fxnn0nninf  10702  seqf1og  10784  1exp  10831  hashinfuni  11040  hashennnuni  11042  hashprg  11073  zfz1isolemiso  11104  cats1un  11306  fisumss  11958  sumsnf  11975  fsumsplitsn  11976  fsum2dlemstep  12000  fisumcom2  12004  fprodssdc  12156  fprodunsn  12170  fprod2dlemstep  12188  fprodcom2fi  12192  fprodsplitsn  12199  divalgmod  12493  phi1  12796  dfphi2  12797  nnnn0modprm0  12833  exmidunben  13052  bassetsnn  13144  gsumress  13483  0nsg  13806  gsumfzsnfd  13937  lsssn0  14390  lspsneq0  14446  txdis1cn  15008  plyaddlem1  15477  plymullem1  15478  plycoeid3  15487  plycj  15491  pw0ss  15940  usgr1vr  16105  bj-nntrans  16572  bj-nnelirr  16574  pwtrufal  16624  sssneq  16629  exmidsbthrlem  16652  gfsumsn  16712