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  11942  summodclem2a  11943  summodc  11945  zsumdc  11946  fsum3  11949  sumsnf  11971  fsumcnv  11999  fisumcom2  12000  fsumshftm  12007  fisum0diag2  12009  prodmodclem3  12137  prodmodclem2a  12138  prodmodc  12140  zproddc  12141  fprodseq  12145  prodsnf  12154  fprodcnv  12187  fprodcom2fi  12188  pcmpt  12917  ctiunctlemu1st  13056  ctiunctlemu2nd  13057  ctiunctlemudc  13059  ctiunctlemfo  13061  prdsex  13353  imasex  13389  psrval  14682  fsumdvdsmul  15717