Theorem csbeq2dv 3865

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

Syntax hints:   → wi 4   = wceq 1541  ⦋csb 3858

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-sbc 3743  df-csb 3859

This theorem is referenced by:  csbeq2i  3866  csbeq12dv  3867  mpomptsx  8001  dmmpossx  8003  fmpox  8004  el2mpocsbcl  8022  offval22  8025  ovmptss  8030  fmpoco  8032  mposn  8040  mpocurryd  8205  fvmpocurryd  8207  cantnffval  9608  fsumcom2  15670  fprodcom2  15878  bpolylem  15942  bpolyval  15943  ruclem1  16124  natfval  17847  fucval  17860  evlfval  18120  mpfrcl  21532  selvffval  21563  selvfval  21564  selvval  21565  pmatcollpw3lem  22169  fsumcn  24270  fsum2cn  24271  dvmptfsum  25376  mulsval  27417  ttgvalOLD  27881  msrfval  34218  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem15  36166  poimirlem18  36169  poimirlem21  36172  poimirlem22  36173  poimirlem24  36175  poimirlem26  36177  poimirlem27  36178  cdleme31sde  38921  cdlemeg47rv2  39046  rnghmval  46309  dmmpossx2  46532