Theorem csbeq2dv 4254

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

Syntax hints:   → wi 4   = wceq 1507  ⦋csb 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-sbc 3681  df-csb 3786

This theorem is referenced by:  csbeq2i  4255  mpomptsx  7567  dmmpossx  7569  fmpox  7570  el2mpocsbcl  7585  offval22  7588  ovmptss  7593  fmpoco  7595  mposn  7603  mpocurryd  7735  fvmpocurryd  7737  cantnffval  8916  fsumcom2  14983  fprodcom2  15192  bpolylem  15256  bpolyval  15257  ruclem1  15438  natfval  17068  fucval  17080  evlfval  17319  mpfrcl  20005  pmatcollpw3lem  21089  fsumcn  23175  fsum2cn  23176  dvmptfsum  24269  ttgval  26358  msrfval  32274  poimirlem5  34316  poimirlem6  34317  poimirlem7  34318  poimirlem8  34319  poimirlem10  34321  poimirlem11  34322  poimirlem12  34323  poimirlem15  34326  poimirlem16  34327  poimirlem17  34328  poimirlem18  34329  poimirlem19  34330  poimirlem20  34331  poimirlem21  34332  poimirlem22  34333  poimirlem24  34335  poimirlem26  34337  poimirlem27  34338  cdleme31sde  36944  cdlemeg47rv2  37069  rnghmval  43500  dmmpt2ssx2  43723