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  6539  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  elixpsn  7022  ixpsnf1o  7023  en1bg  7092  mapsnend  7104  mapsnen  7105  xpassen  7133  fztp  10503  fzsuc2  10504  fseq1p1m1  10519  fseq1m1p1  10520  zfz1isolemsplit  11313  zfz1isolem1  11315  s1val  11408  s1eq  11410  s1prc  11414  fsumm1  12209  fprodm1  12391  divalgmod  12720  ennnfonelemg  13353  ennnfonelemp1  13356  ennnfonelem1  13357  ennnfonelemnn0  13372  setsvalg  13441  strsetsid  13444  imasex  13686  imasival  13687  imasaddvallemg  13696  mulgval  13985  isunitd  14523  lspsnneg  14867  lspsnsub  14868  lmodindp1  14875  lidl0  14936  rsp0  14940  ridl0  14957  zrhrhmb  15067  znval  15081  psrval  15162  txdis  15515  upgr1een  16582  1loopgruspgr  16761  wkslem1  16778  wkslem2  16779  iswlk  16781  loopclwwlkn1b  16877  clwwlkn1loopb  16878  eupth2lem3lem3fi  16928  wexmiddifxylem  17262