Theorem elsni 3418

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

Syntax hints:   → wi 4   = wceq 1285   ∈ wcel 1434  {csn 3400

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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-sn 3406

This theorem is referenced by:  elsn2g  3429  disjsn2  3457  sssnm  3548  disjxsn  3785  opth1  3993  elsuci  4160  ordtri2orexmid  4268  onsucsssucexmid  4272  sosng  4433  ressn  4882  funcnvsn  4969  funinsn  4973  fvconst  5377  fmptap  5379  fmptapd  5380  fvunsng  5383  1stconst  5867  2ndconst  5868  reldmtpos  5896  tpostpos  5907  1domsn  6353  ac6sfi  6421  onunsnss  6427  snon0  6435  supsnti  6467  elreal2  7050  ax1rid  7094  ltxrlt  7234  un0addcl  8377  un0mulcl  8378  elfzonlteqm1  9285  iseqid3  9550  1exp  9591  sizeinfuni  9790  sizeennnuni  9792  sizeprg  9821  divalgmod  10460  bj-nntrans  10889  bj-nnelirr  10891