Theorem csbeq1d 3111

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 3107	. 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 1375   [_csb 3104

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-sbc 3009  df-csb 3105

This theorem is referenced by:  csbidmg  3161  csbco3g  3163  fmptcof  5775  mpomptsx  6313  dmmpossx  6315  fmpox  6316  fmpoco  6332  xpf1o  6973  summodclem3  11857  summodclem2a  11858  summodc  11860  zsumdc  11861  fsum3  11864  sumsnf  11886  fsumcnv  11914  fisumcom2  11915  fsumshftm  11922  fisum0diag2  11924  prodmodclem3  12052  prodmodclem2a  12053  prodmodc  12055  zproddc  12056  fprodseq  12060  prodsnf  12069  fprodcnv  12102  fprodcom2fi  12103  pcmpt  12832  ctiunctlemu1st  12971  ctiunctlemu2nd  12972  ctiunctlemudc  12974  ctiunctlemfo  12976  prdsex  13268  imasex  13304  psrval  14595  fsumdvdsmul  15630