Theorem sneqd 3707

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

Syntax hints:   -> wi 4   = wceq 1398   {csn 3694

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-sn 3700

This theorem is referenced by:  dmsnsnsng  5245  cnvsng  5253  ressn  5308  f1osng  5662  fsng  5855  fsn2g  5857  funopsn  5865  fnressn  5875  fvsng  5885  2nd1st  6387  dfmpo  6432  cnvf1olem  6433  suppsnopdc  6463  tpostpos  6508  tfrlemi1  6576  tfr1onlemaccex  6592  tfrcllemaccex  6605  elixpsn  6983  ixpsnf1o  6984  en1bg  7053  mapsnend  7065  mapsnen  7066  xpassen  7094  fztp  10437  fzsuc2  10438  fseq1p1m1  10453  fseq1m1p1  10454  zfz1isolemsplit  11238  zfz1isolem1  11240  s1val  11333  s1eq  11335  s1prc  11339  fsumm1  12130  fprodm1  12312  divalgmod  12641  ennnfonelemg  13241  ennnfonelemp1  13244  ennnfonelem1  13245  ennnfonelemnn0  13260  setsvalg  13329  strsetsid  13332  imasex  13572  imasival  13573  imasaddvallemg  13582  mulgval  13878  isunitd  14354  lspsnneg  14697  lspsnsub  14698  lmodindp1  14705  lidl0  14766  rsp0  14770  ridl0  14787  zrhrhmb  14899  znval  14913  psrval  14943  txdis  15271  upgr1een  16248  1loopgruspgr  16427  wkslem1  16444  wkslem2  16445  iswlk  16447  loopclwwlkn1b  16543  clwwlkn1loopb  16544  eupth2lem3lem3fi  16594