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  11305  zfz1isolem1  11307  s1val  11400  s1eq  11402  s1prc  11406  fsumm1  12201  fprodm1  12383  divalgmod  12712  ennnfonelemg  13345  ennnfonelemp1  13348  ennnfonelem1  13349  ennnfonelemnn0  13364  setsvalg  13433  strsetsid  13436  imasex  13677  imasival  13678  imasaddvallemg  13687  mulgval  13976  isunitd  14464  lspsnneg  14808  lspsnsub  14809  lmodindp1  14816  lidl0  14877  rsp0  14881  ridl0  14898  zrhrhmb  15008  znval  15022  psrval  15101  txdis  15430  upgr1een  16487  1loopgruspgr  16666  wkslem1  16683  wkslem2  16684  iswlk  16686  loopclwwlkn1b  16782  clwwlkn1loopb  16783  eupth2lem3lem3fi  16833  wexmiddifxylem  17167