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  10487  fzsuc2  10488  fseq1p1m1  10503  fseq1m1p1  10504  zfz1isolemsplit  11292  zfz1isolem1  11294  s1val  11387  s1eq  11389  s1prc  11393  fsumm1  12185  fprodm1  12367  divalgmod  12696  ennnfonelemg  13296  ennnfonelemp1  13299  ennnfonelem1  13300  ennnfonelemnn0  13315  setsvalg  13384  strsetsid  13387  imasex  13628  imasival  13629  imasaddvallemg  13638  mulgval  13927  isunitd  14415  lspsnneg  14759  lspsnsub  14760  lmodindp1  14767  lidl0  14828  rsp0  14832  ridl0  14849  zrhrhmb  14959  znval  14973  psrval  15052  txdis  15380  upgr1een  16377  1loopgruspgr  16556  wkslem1  16573  wkslem2  16574  iswlk  16576  loopclwwlkn1b  16672  clwwlkn1loopb  16673  eupth2lem3lem3fi  16723  wexmiddifxylem  17057