Theorem csbeq2dv 3844

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-12 2175  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-nf 1791  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-sbc 3721  df-csb 3838

This theorem is referenced by:  csbeq2i  3845  csbeq12dv  3846  mpomptsx  7891  dmmpossx  7893  fmpox  7894  el2mpocsbcl  7910  offval22  7913  ovmptss  7918  fmpoco  7920  mposn  7928  mpocurryd  8070  fvmpocurryd  8072  cantnffval  9391  fsumcom2  15476  fprodcom2  15684  bpolylem  15748  bpolyval  15749  ruclem1  15930  natfval  17652  fucval  17665  evlfval  17925  mpfrcl  21285  selvffval  21316  selvfval  21317  selvval  21318  pmatcollpw3lem  21922  fsumcn  24023  fsum2cn  24024  dvmptfsum  25129  ttgvalOLD  27227  msrfval  33487  poimirlem5  35770  poimirlem6  35771  poimirlem7  35772  poimirlem8  35773  poimirlem10  35775  poimirlem11  35776  poimirlem12  35777  poimirlem15  35780  poimirlem18  35783  poimirlem21  35786  poimirlem22  35787  poimirlem24  35789  poimirlem26  35791  poimirlem27  35792  cdleme31sde  38387  cdlemeg47rv2  38512  rnghmval  45410  dmmpossx2  45633