Theorem elsni 3727

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3715

This theorem is used by:  elsn2g  3742  nelsn  3744  disjsn2  3772  rabsnifsb  3777  rabsnif  3778  sssnm  3879  disjxsn  4129  pwntru  4338  opth1  4378  elsuci  4550  ordtri2orexmid  4672  onsucsssucexmid  4676  sosng  4850  elrelimasn  5156  ressn  5331  funcnvsn  5429  funinsn  5433  funopdmsn  5898  fvconst  5906  fmptap  5908  fmptapd  5909  fvunsng  5912  mposnif  6185  1stconst  6461  2ndconst  6462  reldmtpos  6529  tpostpos  6540  1domsn  7121  ac6sfi  7208  elssdc  7215  onunsnss  7230  snon0  7255  snexxph  7274  funisfsuppdc  7298  elfi2  7311  supsnti  7351  djuf1olem  7399  eldju2ndl  7418  eldju2ndr  7419  difinfsnlem  7445  pw1m  7589  pw1on  7591  elreal2  8203  ax1rid  8250  ltxrlt  8397  un0addcl  9607  un0mulcl  9608  fzodisjsn  10607  elfzonlteqm1  10644  xnn0nnen  10894  fxnn0nninf  10896  seqf1og  10978  1exp  11025  hashinfuni  11237  hashennnuni  11239  hashprg  11270  zfz1isolemiso  11312  cats1un  11514  fisumss  12183  sumsnf  12200  fsumsplitsn  12201  fsum2dlemstep  12225  fisumcom2  12229  fprodssdc  12381  fprodunsn  12395  fprod2dlemstep  12413  fprodcom2fi  12417  fprodsplitsn  12424  divalgmod  12718  phi1  13025  dfphi2  13026  nnnn0modprm0  13062  exmidunben  13374  bassetsnn  13466  gzsumress  13770  0nsg  14075  gzsumsnfd  14236  gsumsncmn  14245  gsummptfidmsplit  14253  gsumsnfdcmn  14256  gsumunsnfd  14258  gsum2dfilem2  14271  lsssn0  14815  lspsneq0  14871  gsumfsum  15031  mplsubgfilemcl  15232  mplsubgfileminv  15233  txdis1cn  15521  plyaddlem1  15990  plymullem1  15991  plycoeid3  16000  plycj  16004  pw0ss  16546  usgr1vr  16711  bj-nntrans  17199  bj-nnelirr  17201  pwtrufal  17249  sssneq  17254  wexmiddifxylem  17267  idjudju  17269  exmidsbthrlem  17290