Theorem elsni 3691

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2202  {csn 3673

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-sn 3679

This theorem is referenced by:  elsn2g  3706  nelsn  3708  disjsn2  3736  rabsnifsb  3741  rabsnif  3742  sssnm  3842  disjxsn  4091  pwntru  4295  opth1  4334  elsuci  4506  ordtri2orexmid  4627  onsucsssucexmid  4631  sosng  4805  elrelimasn  5109  ressn  5284  funcnvsn  5382  funinsn  5386  funopdmsn  5842  fvconst  5850  fmptap  5852  fmptapd  5853  fvunsng  5856  mposnif  6125  1stconst  6395  2ndconst  6396  reldmtpos  6462  tpostpos  6473  1domsn  7044  ac6sfi  7130  elssdc  7137  onunsnss  7152  snon0  7177  snexxph  7192  elfi2  7214  supsnti  7247  djuf1olem  7295  eldju2ndl  7314  eldju2ndr  7315  difinfsnlem  7341  pw1m  7485  pw1on  7487  elreal2  8093  ax1rid  8140  ltxrlt  8287  un0addcl  9477  un0mulcl  9478  fzodisjsn  10464  elfzonlteqm1  10501  xnn0nnen  10745  fxnn0nninf  10747  seqf1og  10829  1exp  10876  hashinfuni  11085  hashennnuni  11087  hashprg  11118  zfz1isolemiso  11149  cats1un  11351  fisumss  12016  sumsnf  12033  fsumsplitsn  12034  fsum2dlemstep  12058  fisumcom2  12062  fprodssdc  12214  fprodunsn  12228  fprod2dlemstep  12246  fprodcom2fi  12250  fprodsplitsn  12257  divalgmod  12551  phi1  12854  dfphi2  12855  nnnn0modprm0  12891  exmidunben  13110  bassetsnn  13202  gsumress  13541  0nsg  13864  gsumfzsnfd  13995  lsssn0  14449  lspsneq0  14505  txdis1cn  15072  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plycj  15555  pw0ss  16007  usgr1vr  16172  bj-nntrans  16650  bj-nnelirr  16652  pwtrufal  16702  sssneq  16707  exmidsbthrlem  16733  gfsumsn  16797