Theorem csbeq2dv 3835

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712  df-csb 3829

This theorem is referenced by:  csbeq2i  3836  csbeq12dv  3837  mpomptsx  7877  dmmpossx  7879  fmpox  7880  el2mpocsbcl  7896  offval22  7899  ovmptss  7904  fmpoco  7906  mposn  7914  mpocurryd  8056  fvmpocurryd  8058  cantnffval  9351  fsumcom2  15414  fprodcom2  15622  bpolylem  15686  bpolyval  15687  ruclem1  15868  natfval  17578  fucval  17591  evlfval  17851  mpfrcl  21205  selvffval  21236  selvfval  21237  selvval  21238  pmatcollpw3lem  21840  fsumcn  23939  fsum2cn  23940  dvmptfsum  25044  ttgval  27140  msrfval  33399  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  cdleme31sde  38326  cdlemeg47rv2  38451  rnghmval  45337  dmmpossx2  45560