Theorem sneqd 3722

Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.)

Hypothesis

Ref	Expression
sneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sneqd	⊢ (𝜑 → {𝐴} = {𝐵})

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sneq 3720	. 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
3	1, 2	syl 14	1 ⊢ (𝜑 → {𝐴} = {𝐵})

This proof depends on syntax axioms:   → wi 4   = wceq 1402  {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3715

This theorem is used by:  dmsnsnsng  5268  cnvsng  5276  ressn  5331  f1osng  5685  fsng  5884  fsn2g  5886  funopsn  5894  fnressn  5904  fvsng  5914  2nd1st  6418  dfmpo  6463  cnvf1olem  6464  suppsnopdc  6494  tpostpos  6539  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  elixpsn  7021  ixpsnf1o  7022  en1bg  7091  mapsnend  7103  mapsnen  7104  xpassen  7132  fztp  10502  fzsuc2  10503  fseq1p1m1  10518  fseq1m1p1  10519  zfz1isolemsplit  11312  zfz1isolem1  11314  s1val  11407  s1eq  11409  s1prc  11413  fsumm1  12208  fprodm1  12390  divalgmod  12719  ennnfonelemg  13352  ennnfonelemp1  13355  ennnfonelem1  13356  ennnfonelemnn0  13371  setsvalg  13440  strsetsid  13443  imasex  13685  imasival  13686  imasaddvallemg  13695  mulgval  13984  isunitd  14522  lspsnneg  14866  lspsnsub  14867  lmodindp1  14874  lidl0  14935  rsp0  14939  ridl0  14956  zrhrhmb  15066  znval  15080  psrval  15159  txdis  15503  upgr1een  16570  1loopgruspgr  16749  wkslem1  16766  wkslem2  16767  iswlk  16769  loopclwwlkn1b  16865  clwwlkn1loopb  16866  eupth2lem3lem3fi  16916  wexmiddifxylem  17250