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  5833  fvconst  5841  fmptap  5843  fmptapd  5844  fvunsng  5847  mposnif  6114  1stconst  6385  2ndconst  6386  reldmtpos  6418  tpostpos  6429  1domsn  7000  ac6sfi  7086  elssdc  7093  onunsnss  7108  snon0  7133  snexxph  7148  elfi2  7170  supsnti  7203  djuf1olem  7251  eldju2ndl  7270  eldju2ndr  7271  difinfsnlem  7297  pw1m  7441  pw1on  7443  elreal2  8049  ax1rid  8096  ltxrlt  8244  un0addcl  9434  un0mulcl  9435  fzodisjsn  10418  elfzonlteqm1  10454  xnn0nnen  10698  fxnn0nninf  10700  seqf1og  10782  1exp  10829  hashinfuni  11038  hashennnuni  11040  hashprg  11071  zfz1isolemiso  11102  cats1un  11301  fisumss  11952  sumsnf  11969  fsumsplitsn  11970  fsum2dlemstep  11994  fisumcom2  11998  fprodssdc  12150  fprodunsn  12164  fprod2dlemstep  12182  fprodcom2fi  12186  fprodsplitsn  12193  divalgmod  12487  phi1  12790  dfphi2  12791  nnnn0modprm0  12827  exmidunben  13046  bassetsnn  13138  gsumress  13477  0nsg  13800  gsumfzsnfd  13931  lsssn0  14383  lspsneq0  14439  txdis1cn  15001  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycj  15484  pw0ss  15933  usgr1vr  16098  bj-nntrans  16546  bj-nnelirr  16548  pwtrufal  16598  sssneq  16603  exmidsbthrlem  16626