Theorem csbeq1d 3134

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 3130	. 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 1397   [_csb 3127

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-clel 2227  df-sbc 3032  df-csb 3128

This theorem is referenced by:  csbidmg  3184  csbco3g  3186  fmptcof  5814  mpomptsx  6362  dmmpossx  6364  fmpox  6365  fmpoco  6381  xpf1o  7030  summodclem3  11943  summodclem2a  11944  summodc  11946  zsumdc  11947  fsum3  11950  sumsnf  11972  fsumcnv  12000  fisumcom2  12001  fsumshftm  12008  fisum0diag2  12010  prodmodclem3  12138  prodmodclem2a  12139  prodmodc  12141  zproddc  12142  fprodseq  12146  prodsnf  12155  fprodcnv  12188  fprodcom2fi  12189  pcmpt  12918  ctiunctlemu1st  13057  ctiunctlemu2nd  13058  ctiunctlemudc  13060  ctiunctlemfo  13062  prdsex  13354  imasex  13390  psrval  14683  fsumdvdsmul  15718