Theorem elsni 3492

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

Syntax hints:   → wi 4   = wceq 1299   ∈ wcel 1448  {csn 3474

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-sn 3480

This theorem is referenced by:  elsn2g  3505  disjsn2  3533  sssnm  3628  disjxsn  3873  opth1  4096  elsuci  4263  ordtri2orexmid  4376  onsucsssucexmid  4380  sosng  4550  ressn  5015  funcnvsn  5104  funinsn  5108  fvconst  5540  fmptap  5542  fmptapd  5543  fvunsng  5546  mposnif  5797  1stconst  6048  2ndconst  6049  reldmtpos  6080  tpostpos  6091  1domsn  6642  ac6sfi  6721  onunsnss  6734  snon0  6752  snexxph  6766  supsnti  6807  djuf1olem  6853  eldju2ndl  6872  eldju2ndr  6873  difinfsnlem  6899  elreal2  7518  ax1rid  7562  ltxrlt  7702  un0addcl  8862  un0mulcl  8863  elfzonlteqm1  9828  fxnn0nninf  10052  1exp  10163  hashinfuni  10364  hashennnuni  10366  hashprg  10395  zfz1isolemiso  10423  fisumss  11000  sumsnf  11017  fsumsplitsn  11018  fsum2dlemstep  11042  fisumcom2  11046  divalgmod  11419  phi1  11687  dfphi2  11688  exmidunben  11731  txdis1cn  12228  bj-nntrans  12734  bj-nnelirr  12736  pwtrufal  12777  pwntru  12778  exmidsbthrlem  12801