Theorem csbeq1d 3056

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 3052	. 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 1348   [_csb 3049

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956  df-csb 3050

This theorem is referenced by:  csbidmg  3105  csbco3g  3107  fmptcof  5663  mpomptsx  6176  dmmpossx  6178  fmpox  6179  fmpoco  6195  xpf1o  6822  summodclem3  11343  summodclem2a  11344  summodc  11346  zsumdc  11347  fsum3  11350  sumsnf  11372  fsumcnv  11400  fisumcom2  11401  fsumshftm  11408  fisum0diag2  11410  prodmodclem3  11538  prodmodclem2a  11539  prodmodc  11541  zproddc  11542  fprodseq  11546  prodsnf  11555  fprodcnv  11588  fprodcom2fi  11589  pcmpt  12295  ctiunctlemu1st  12389  ctiunctlemu2nd  12390  ctiunctlemudc  12392  ctiunctlemfo  12394