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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   [_csb 3147

This proof depends on 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 proof 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 used by:  csbidmg  3204  csbco3g  3206  fmptcof  5875  mpomptsx  6433  dmmpossx  6435  fmpox  6436  fmpoco  6452  xpf1o  7144  summodclem3  12163  summodclem2a  12164  summodc  12166  zsumdc  12167  fsum3  12170  sumsnf  12192  fsumcnv  12220  fisumcom2  12221  fsumshftm  12228  fisum0diag2  12230  prodmodclem3  12358  prodmodclem2a  12359  prodmodc  12361  zproddc  12362  fprodseq  12366  prodsnf  12375  fprodcnv  12408  fprodcom2fi  12409  pcmpt  13142  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  imasex  13675  prdsex  14221  psrval  15099  fsumdvdsmul  16204