Theorem elsni 3588

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

Syntax hints:   → wi 4   = wceq 1342   ∈ wcel 2135  {csn 3570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-sn 3576

This theorem is referenced by:  elsn2g  3603  nelsn  3605  disjsn2  3633  sssnm  3728  disjxsn  3974  pwntru  4172  opth1  4208  elsuci  4375  ordtri2orexmid  4494  onsucsssucexmid  4498  sosng  4671  ressn  5138  funcnvsn  5227  funinsn  5231  fvconst  5667  fmptap  5669  fmptapd  5670  fvunsng  5673  mposnif  5927  1stconst  6180  2ndconst  6181  reldmtpos  6212  tpostpos  6223  1domsn  6776  ac6sfi  6855  onunsnss  6873  snon0  6892  snexxph  6906  elfi2  6928  supsnti  6961  djuf1olem  7009  eldju2ndl  7028  eldju2ndr  7029  difinfsnlem  7055  pw1on  7173  elreal2  7762  ax1rid  7809  ltxrlt  7955  un0addcl  9138  un0mulcl  9139  elfzonlteqm1  10135  fxnn0nninf  10363  1exp  10474  hashinfuni  10679  hashennnuni  10681  hashprg  10710  zfz1isolemiso  10738  fisumss  11319  sumsnf  11336  fsumsplitsn  11337  fsum2dlemstep  11361  fisumcom2  11365  fprodssdc  11517  fprodunsn  11531  fprod2dlemstep  11549  fprodcom2fi  11553  fprodsplitsn  11560  divalgmod  11849  phi1  12128  dfphi2  12129  nnnn0modprm0  12164  exmidunben  12296  txdis1cn  12819  bj-nntrans  13668  bj-nnelirr  13670  pwtrufal  13711  sssneq  13716  exmidsbthrlem  13735