Theorem csbeq1d 3540

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 3536	. 2 |- ( A = B -> [_ A / x ]_ C = [_ B / x ]_ C )
3	1, 2	syl 17	1 |- ( ph -> [_ A / x ]_ C = [_ B / x ]_ C )

Syntax hints:   -> wi 4   = wceq 1483   [_csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436  df-csb 3534

This theorem is referenced by:  csbco3g  4000  csbidm  4002  fmptcof  6397  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  ovmptss  7258  fmpt2co  7260  xpf1o  8122  hsmexlem2  9249  iundom2g  9362  sumeq2ii  14423  summolem3  14445  summolem2a  14446  summo  14448  zsum  14449  fsum  14451  sumsnf  14473  sumsn  14475  fsumcnv  14504  fsumcom2  14505  fsumcom2OLD  14506  fsumshftm  14513  fsum0diag2  14515  prodeq2ii  14643  prodmolem3  14663  prodmolem2a  14664  prodmo  14666  zprod  14667  fprod  14671  prodsn  14692  prodsnf  14694  fprodcnv  14713  fprodcom2  14714  fprodcom2OLD  14715  bpolylem  14779  bpolyval  14780  ruclem1  14960  pcmpt  15596  gsumvalx  17270  odfval  17952  odval  17953  telgsumfzslem  18385  telgsumfzs  18386  psrval  19362  psrass1lem  19377  mpfrcl  19518  evlsval  19519  evls1fval  19684  fsum2cn  22674  iunmbl2  23325  dvfsumlem1  23789  itgsubst  23812  q1pval  23913  r1pval  23916  rlimcnp2  24693  fsumdvdscom  24911  fsumdvdsmul  24921  ttgval  25755  fsumiunle  29575  msrfval  31434  poimirlem1  33410  poimirlem3  33412  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  fsumshftdOLD  34238  cdleme31snd  35674  cdlemeg46c  35801  cdlemkid2  36212  cdlemk46  36236  cdlemk53b  36244  cdlemk53  36245  monotuz  37506  oddcomabszz  37509  fnwe2val  37619  fnwe2lem1  37620  fnwe2lem2  37621  mendval  37753  sumsnd  39185  climinf2mpt  39946  climinfmpt  39947  sge0f1o  40599  rnghmval  41891  dmmpt2ssx2  42115