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  6540  tfrlemi1  6608  tfr1onlemaccex  6624  tfrcllemaccex  6637  elixpsn  7023  ixpsnf1o  7024  en1bg  7093  mapsnend  7105  mapsnen  7106  xpassen  7134  fztp  10501  fzsuc2  10502  fseq1p1m1  10517  fseq1m1p1  10518  zfz1isolemsplit  11311  zfz1isolem1  11313  s1val  11406  s1eq  11408  s1prc  11412  fsumm1  12207  fprodm1  12389  divalgmod  12718  ennnfonelemg  13351  ennnfonelemp1  13354  ennnfonelem1  13355  ennnfonelemnn0  13370  setsvalg  13439  strsetsid  13442  imasex  13684  imasival  13685  imasaddvallemg  13694  mulgval  13983  isunitd  14521  lspsnneg  14865  lspsnsub  14866  lmodindp1  14873  lidl0  14934  rsp0  14938  ridl0  14955  zrhrhmb  15065  znval  15079  psrval  15160  txdis  15520  upgr1een  16587  1loopgruspgr  16766  wkslem1  16783  wkslem2  16784  iswlk  16786  loopclwwlkn1b  16882  clwwlkn1loopb  16883  eupth2lem3lem3fi  16933  wexmiddifxylem  17267