Theorem elsni 3449

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

Syntax hints:   → wi 4   = wceq 1287   ∈ wcel 1436  {csn 3431

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-sn 3437

This theorem is referenced by:  elsn2g  3462  disjsn2  3490  sssnm  3583  disjxsn  3820  opth1  4039  elsuci  4206  ordtri2orexmid  4314  onsucsssucexmid  4318  sosng  4481  ressn  4939  funcnvsn  5026  funinsn  5030  fvconst  5450  fmptap  5452  fmptapd  5453  fvunsng  5456  1stconst  5945  2ndconst  5946  reldmtpos  5974  tpostpos  5985  1domsn  6489  ac6sfi  6568  onunsnss  6581  snon0  6598  snexxph  6611  supsnti  6647  djuf1olem  6692  djur  6704  eldju2ndl  6710  eldju2ndr  6711  elreal2  7315  ax1rid  7359  ltxrlt  7499  un0addcl  8642  un0mulcl  8643  elfzonlteqm1  9552  fxnn0nninf  9775  iseqid3  9844  1exp  9886  hashinfuni  10085  hashennnuni  10087  hashprg  10116  zfz1isolemiso  10144  fisumss  10675  sumsnf  10691  divalgmod  10833  phi1  11101  dfphi2  11102  bj-nntrans  11315  bj-nnelirr  11317  exmidsbthrlem  11381