Theorem sneqd 3682

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 3680	. 2 |- ( A = B -> { A } = { B } )
3	1, 2	syl 14	1 |- ( ph -> { A } = { B } )

Syntax hints:   -> wi 4   = wceq 1397   {csn 3669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-sn 3675

This theorem is referenced by:  dmsnsnsng  5214  cnvsng  5222  ressn  5277  f1osng  5626  fsng  5820  fsn2g  5822  funopsn  5830  fnressn  5840  fvsng  5850  2nd1st  6343  dfmpo  6388  cnvf1olem  6389  tpostpos  6430  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  elixpsn  6904  ixpsnf1o  6905  en1bg  6974  mapsnen  6986  xpassen  7014  fztp  10313  fzsuc2  10314  fseq1p1m1  10329  fseq1m1p1  10330  zfz1isolemsplit  11103  zfz1isolem1  11105  s1val  11195  s1eq  11197  s1prc  11201  fsumm1  11979  fprodm1  12161  divalgmod  12490  ennnfonelemg  13026  ennnfonelemp1  13029  ennnfonelem1  13030  ennnfonelemnn0  13045  setsvalg  13114  strsetsid  13117  imasex  13390  imasival  13391  imasaddvallemg  13400  mulgval  13711  isunitd  14123  lspsnneg  14437  lspsnsub  14438  lmodindp1  14445  lidl0  14506  rsp0  14510  ridl0  14527  zrhrhmb  14639  znval  14653  psrval  14683  txdis  15004  upgr1een  15978  1loopgruspgr  16157  wkslem1  16174  wkslem2  16175  iswlk  16177  loopclwwlkn1b  16273  clwwlkn1loopb  16274  eupth2lem3lem3fi  16324