Theorem sneqd 3721

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

Syntax hints:   -> wi 4   = wceq 1402   {csn 3708

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 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 theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-sn 3714

This theorem is referenced by:  dmsnsnsng  5263  cnvsng  5271  ressn  5326  f1osng  5680  fsng  5875  fsn2g  5877  funopsn  5885  fnressn  5895  fvsng  5905  2nd1st  6408  dfmpo  6453  cnvf1olem  6454  suppsnopdc  6484  tpostpos  6529  tfrlemi1  6597  tfr1onlemaccex  6613  tfrcllemaccex  6626  elixpsn  7011  ixpsnf1o  7012  en1bg  7081  mapsnend  7093  mapsnen  7094  xpassen  7122  fztp  10468  fzsuc2  10469  fseq1p1m1  10484  fseq1m1p1  10485  zfz1isolemsplit  11273  zfz1isolem1  11275  s1val  11368  s1eq  11370  s1prc  11374  fsumm1  12166  fprodm1  12348  divalgmod  12677  ennnfonelemg  13277  ennnfonelemp1  13280  ennnfonelem1  13281  ennnfonelemnn0  13296  setsvalg  13365  strsetsid  13368  imasex  13609  imasival  13610  imasaddvallemg  13619  mulgval  13908  isunitd  14396  lspsnneg  14740  lspsnsub  14741  lmodindp1  14748  lidl0  14809  rsp0  14813  ridl0  14830  zrhrhmb  14940  znval  14954  psrval  15033  txdis  15361  upgr1een  16348  1loopgruspgr  16527  wkslem1  16544  wkslem2  16545  iswlk  16547  loopclwwlkn1b  16643  clwwlkn1loopb  16644  eupth2lem3lem3fi  16694