Theorem elsni 3625

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2160  {csn 3607

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-sn 3613

This theorem is referenced by:  elsn2g  3640  nelsn  3642  disjsn2  3670  sssnm  3769  disjxsn  4016  pwntru  4217  opth1  4254  elsuci  4421  ordtri2orexmid  4540  onsucsssucexmid  4544  sosng  4717  elrelimasn  5012  ressn  5187  funcnvsn  5280  funinsn  5284  fvconst  5725  fmptap  5727  fmptapd  5728  fvunsng  5731  mposnif  5991  1stconst  6247  2ndconst  6248  reldmtpos  6279  tpostpos  6290  1domsn  6846  ac6sfi  6927  onunsnss  6946  snon0  6966  snexxph  6980  elfi2  7002  supsnti  7035  djuf1olem  7083  eldju2ndl  7102  eldju2ndr  7103  difinfsnlem  7129  pw1on  7256  elreal2  7860  ax1rid  7907  ltxrlt  8054  un0addcl  9240  un0mulcl  9241  elfzonlteqm1  10242  fxnn0nninf  10471  1exp  10583  hashinfuni  10792  hashennnuni  10794  hashprg  10823  zfz1isolemiso  10854  fisumss  11435  sumsnf  11452  fsumsplitsn  11453  fsum2dlemstep  11477  fisumcom2  11481  fprodssdc  11633  fprodunsn  11647  fprod2dlemstep  11665  fprodcom2fi  11669  fprodsplitsn  11676  divalgmod  11967  phi1  12254  dfphi2  12255  nnnn0modprm0  12290  exmidunben  12480  gsumress  12873  0nsg  13170  lsssn0  13703  lspsneq0  13759  txdis1cn  14255  bj-nntrans  15181  bj-nnelirr  15183  pwtrufal  15226  sssneq  15230  exmidsbthrlem  15249