Theorem sneqd 3722

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

Hypothesis

Ref	Expression
sneqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sneqd	|- ( ph -> { A } = { B } )

Proof of Theorem sneqd

Step	Hyp	Ref	Expression
1		sneqd.1	. 2 |- ( ph -> A = B )
2		sneq 3720	. 2 |- ( A = B -> { A } = { B } )
3	1, 2	syl 14	1 |- ( ph -> { A } = { B } )

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  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  15161  txdis  15536  upgr1een  16603  1loopgruspgr  16782  wkslem1  16799  wkslem2  16800  iswlk  16802  loopclwwlkn1b  16898  clwwlkn1loopb  16899  eupth2lem3lem3fi  16949  wexmiddifxylem  17283