Theorem csbeq1d 3131

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 3127	. 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 1395   [_csb 3124

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3029  df-csb 3125

This theorem is referenced by:  csbidmg  3181  csbco3g  3183  fmptcof  5807  mpomptsx  6354  dmmpossx  6356  fmpox  6357  fmpoco  6373  xpf1o  7018  summodclem3  11912  summodclem2a  11913  summodc  11915  zsumdc  11916  fsum3  11919  sumsnf  11941  fsumcnv  11969  fisumcom2  11970  fsumshftm  11977  fisum0diag2  11979  prodmodclem3  12107  prodmodclem2a  12108  prodmodc  12110  zproddc  12111  fprodseq  12115  prodsnf  12124  fprodcnv  12157  fprodcom2fi  12158  pcmpt  12887  ctiunctlemu1st  13026  ctiunctlemu2nd  13027  ctiunctlemudc  13029  ctiunctlemfo  13031  prdsex  13323  imasex  13359  psrval  14651  fsumdvdsmul  15686