Theorem csbeq2dv 3835

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

Hypothesis

Ref	Expression
csbeq2dv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
csbeq2dv	⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem csbeq2dv

Step	Hyp	Ref	Expression
1		nfv 1915	. 2 ⊢ Ⅎ𝑥𝜑
2		csbeq2dv.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	csbeq2d 3834	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1538  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721  df-csb 3829

This theorem is referenced by:  csbeq2i  3836  csbeq12dv  3837  mpomptsx  7744  dmmpossx  7746  fmpox  7747  el2mpocsbcl  7763  offval22  7766  ovmptss  7771  fmpoco  7773  mposn  7781  mpocurryd  7918  fvmpocurryd  7920  cantnffval  9110  fsumcom2  15121  fprodcom2  15330  bpolylem  15394  bpolyval  15395  ruclem1  15576  natfval  17208  fucval  17220  evlfval  17459  mpfrcl  20757  selvffval  20788  selvfval  20789  selvval  20790  pmatcollpw3lem  21388  fsumcn  23475  fsum2cn  23476  dvmptfsum  24578  ttgval  26669  msrfval  32897  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  cdleme31sde  37681  cdlemeg47rv2  37806  rnghmval  44515  dmmpossx2  44738