Theorem csbeq1d 3038

Description: Equality deduction for proper substitution into a class. (Contributed by NM, 3-Dec-2005.)

Hypothesis

Ref	Expression
csbeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
csbeq1d	|- ( ph -> [_ A / x ]_ C = [_ B / x ]_ C )

Proof of Theorem csbeq1d

Step	Hyp	Ref	Expression
1		csbeq1d.1	. 2 |- ( ph -> A = B )
2		csbeq1 3034	. 2 |- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
3	1, 2	syl 14	1 |- ( ph -> [_ A / x ]_ C = [_ B / x ]_ C )

Syntax hints:   -> wi 4   = wceq 1335   [_csb 3031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-sbc 2938  df-csb 3032

This theorem is referenced by:  csbidmg  3087  csbco3g  3089  fmptcof  5635  mpomptsx  6146  dmmpossx  6148  fmpox  6149  fmpoco  6164  xpf1o  6790  summodclem3  11281  summodclem2a  11282  summodc  11284  zsumdc  11285  fsum3  11288  sumsnf  11310  fsumcnv  11338  fisumcom2  11339  fsumshftm  11346  fisum0diag2  11348  prodmodclem3  11476  prodmodclem2a  11477  prodmodc  11479  zproddc  11480  fprodseq  11484  prodsnf  11493  fprodcnv  11526  fprodcom2fi  11527  ctiunctlemu1st  12205  ctiunctlemu2nd  12206  ctiunctlemudc  12208  ctiunctlemfo  12210