Theorem csbeq1d 3154

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 3150	. 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 1402   [_csb 3147

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052  df-csb 3148

This theorem is referenced by:  csbidmg  3204  csbco3g  3206  fmptcof  5869  mpomptsx  6427  dmmpossx  6429  fmpox  6430  fmpoco  6446  xpf1o  7138  summodclem3  12130  summodclem2a  12131  summodc  12133  zsumdc  12134  fsum3  12137  sumsnf  12159  fsumcnv  12187  fisumcom2  12188  fsumshftm  12195  fisum0diag2  12197  prodmodclem3  12325  prodmodclem2a  12326  prodmodc  12328  zproddc  12329  fprodseq  12333  prodsnf  12342  fprodcnv  12375  fprodcom2fi  12376  pcmpt  13105  ctiunctlemu1st  13308  ctiunctlemu2nd  13309  ctiunctlemudc  13311  ctiunctlemfo  13313  imasex  13609  prdsex  14155  psrval  15033  fsumdvdsmul  16088