Theorem csbeq2dv 3992

Description: Formula-building deduction rule for class substitution. (Contributed by NM, 10-Nov-2005.) (Revised by Mario Carneiro, 1-Sep-2015.)

Hypothesis

Ref	Expression
csbeq2dv.1	|- ( ph -> B = C )

Assertion

Ref	Expression
csbeq2dv	|- ( ph -> [_ A / x ]_ B = [_ A / x ]_ C )

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem csbeq2dv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		csbeq2dv.1	. 2 |- ( ph -> B = C )
3	1, 2	csbeq2d 3991	1 |- ( ph -> [_ A / x ]_ B = [_ A / 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:  csbeq2i  3993  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  el2mpt2csbcl  7250  offval22  7253  ovmptss  7258  fmpt2co  7260  mpt2sn  7268  mpt2curryd  7395  fvmpt2curryd  7397  cantnffval  8560  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  bpolylem  14779  bpolyval  14780  ruclem1  14960  natfval  16606  fucval  16618  evlfval  16857  mpfrcl  19518  pmatcollpw3lem  20588  fsumcn  22673  fsum2cn  22674  dvmptfsum  23738  ttgval  25755  msrfval  31434  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  poimirlem24  33433  poimirlem26  33435  poimirlem27  33436  cdleme31sde  35673  cdlemeg47rv2  35798  rnghmval  41891  dmmpt2ssx2  42115