Theorem sneqd 3487

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

Syntax hints:   -> wi 4   = wceq 1299   {csn 3474

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-sn 3480

This theorem is referenced by:  dmsnsnsng  4952  cnvsng  4960  ressn  5015  f1osng  5342  fsng  5525  fnressn  5538  fvsng  5548  2nd1st  6008  dfmpo  6050  cnvf1olem  6051  tpostpos  6091  tfrlemi1  6159  tfr1onlemaccex  6175  tfrcllemaccex  6188  elixpsn  6559  ixpsnf1o  6560  en1bg  6624  mapsnen  6635  xpassen  6653  fztp  9699  fzsuc2  9700  fseq1p1m1  9715  fseq1m1p1  9716  zfz1isolemsplit  10422  zfz1isolem1  10424  fsumm1  11024  divalgmod  11419  ennnfonelemg  11708  ennnfonelemp1  11711  ennnfonelem1  11712  ennnfonelemnn0  11727  setsvalg  11771  strsetsid  11774  txdis  12227