Theorem csbeq2dv 3901

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 1918	. 2 ⊢ Ⅎ𝑥𝜑
2		csbeq2dv.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	csbeq2d 3900	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1542  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbeq2i  3902  csbeq12dv  3903  mpomptsx  8050  dmmpossx  8052  fmpox  8053  el2mpocsbcl  8071  offval22  8074  ovmptss  8079  fmpoco  8081  mposn  8089  mpocurryd  8254  fvmpocurryd  8256  cantnffval  9658  fsumcom2  15720  fprodcom2  15928  bpolylem  15992  bpolyval  15993  ruclem1  16174  natfval  17897  fucval  17910  evlfval  18170  mpfrcl  21648  selvffval  21679  selvfval  21680  selvval  21681  pmatcollpw3lem  22285  fsumcn  24386  fsum2cn  24387  dvmptfsum  25492  mulsval  27565  precsexlemcbv  27652  ttgvalOLD  28127  msrfval  34528  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  poimirlem24  36512  poimirlem26  36514  poimirlem27  36515  cdleme31sde  39256  cdlemeg47rv2  39381  rnghmval  46689  dmmpossx2  47012