Theorem csbeq2dv 3897

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

Syntax hints:   → wi 4   = wceq 1533  ⦋csb 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3775  df-csb 3891

This theorem is referenced by:  csbeq2i  3898  csbeq12dv  3899  mpomptsx  8067  dmmpossx  8069  fmpox  8070  el2mpocsbcl  8088  offval22  8091  ovmptss  8096  fmpoco  8098  mposn  8106  mpocurryd  8273  fvmpocurryd  8275  cantnffval  9686  fsumcom2  15752  fprodcom2  15960  bpolylem  16024  bpolyval  16025  ruclem1  16207  natfval  17935  fucval  17948  evlfval  18208  rnghmval  20383  mpfrcl  22038  selvffval  22066  selvfval  22067  selvval  22068  pmatcollpw3lem  22715  fsumcn  24818  fsum2cn  24819  dvmptfsum  25937  mulsval  28043  precsexlemcbv  28138  ttgvalOLD  28736  msrfval  35217  poimirlem5  37168  poimirlem6  37169  poimirlem7  37170  poimirlem8  37171  poimirlem10  37173  poimirlem11  37174  poimirlem12  37175  poimirlem15  37178  poimirlem18  37181  poimirlem21  37184  poimirlem22  37185  poimirlem24  37187  poimirlem26  37189  poimirlem27  37190  cdleme31sde  39927  cdlemeg47rv2  40052  dmmpossx2  47512