Theorem csbeq2dv 3899

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 3898	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1539  ⦋csb 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-sbc 3777  df-csb 3893

This theorem is referenced by:  csbeq2i  3900  csbeq12dv  3901  mpomptsx  8052  dmmpossx  8054  fmpox  8055  el2mpocsbcl  8073  offval22  8076  ovmptss  8081  fmpoco  8083  mposn  8091  mpocurryd  8256  fvmpocurryd  8258  cantnffval  9660  fsumcom2  15724  fprodcom2  15932  bpolylem  15996  bpolyval  15997  ruclem1  16178  natfval  17901  fucval  17914  evlfval  18174  rnghmval  20331  mpfrcl  21867  selvffval  21898  selvfval  21899  selvval  21900  pmatcollpw3lem  22505  fsumcn  24608  fsum2cn  24609  dvmptfsum  25727  mulsval  27804  precsexlemcbv  27891  ttgvalOLD  28394  msrfval  34826  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  poimirlem18  36809  poimirlem21  36812  poimirlem22  36813  poimirlem24  36815  poimirlem26  36817  poimirlem27  36818  cdleme31sde  39559  cdlemeg47rv2  39684  dmmpossx2  47100