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  5265  cnvsng  5273  ressn  5328  f1osng  5682  fsng  5881  fsn2g  5883  funopsn  5891  fnressn  5901  fvsng  5911  2nd1st  6414  dfmpo  6459  cnvf1olem  6460  suppsnopdc  6490  tpostpos  6535  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  elixpsn  7017  ixpsnf1o  7018  en1bg  7087  mapsnend  7099  mapsnen  7100  xpassen  7128  fztp  10496  fzsuc2  10497  fseq1p1m1  10512  fseq1m1p1  10513  zfz1isolemsplit  11306  zfz1isolem1  11308  s1val  11401  s1eq  11403  s1prc  11407  fsumm1  12202  fprodm1  12384  divalgmod  12713  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelem1  13350  ennnfonelemnn0  13365  setsvalg  13434  strsetsid  13437  imasex  13679  imasival  13680  imasaddvallemg  13689  mulgval  13978  isunitd  14504  lspsnneg  14848  lspsnsub  14849  lmodindp1  14856  lidl0  14917  rsp0  14921  ridl0  14938  zrhrhmb  15048  znval  15062  psrval  15141  txdis  15477  upgr1een  16544  1loopgruspgr  16723  wkslem1  16740  wkslem2  16741  iswlk  16743  loopclwwlkn1b  16839  clwwlkn1loopb  16840  eupth2lem3lem3fi  16890  wexmiddifxylem  17224