Theorem csbeq1d 3076

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 3072	. 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 1363   [_csb 3069

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-sbc 2975  df-csb 3070

This theorem is referenced by:  csbidmg  3125  csbco3g  3127  fmptcof  5696  mpomptsx  6212  dmmpossx  6214  fmpox  6215  fmpoco  6231  xpf1o  6858  summodclem3  11402  summodclem2a  11403  summodc  11405  zsumdc  11406  fsum3  11409  sumsnf  11431  fsumcnv  11459  fisumcom2  11460  fsumshftm  11467  fisum0diag2  11469  prodmodclem3  11597  prodmodclem2a  11598  prodmodc  11600  zproddc  11601  fprodseq  11605  prodsnf  11614  fprodcnv  11647  fprodcom2fi  11648  pcmpt  12355  ctiunctlemu1st  12449  ctiunctlemu2nd  12450  ctiunctlemudc  12452  ctiunctlemfo  12454  prdsex  12736  imasex  12744