Theorem csbeq2dv 3839

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717  df-csb 3833

This theorem is referenced by:  csbeq2i  3840  csbeq12dv  3841  mpomptsx  7904  dmmpossx  7906  fmpox  7907  el2mpocsbcl  7925  offval22  7928  ovmptss  7933  fmpoco  7935  mposn  7943  mpocurryd  8085  fvmpocurryd  8087  cantnffval  9421  fsumcom2  15486  fprodcom2  15694  bpolylem  15758  bpolyval  15759  ruclem1  15940  natfval  17662  fucval  17675  evlfval  17935  mpfrcl  21295  selvffval  21326  selvfval  21327  selvval  21328  pmatcollpw3lem  21932  fsumcn  24033  fsum2cn  24034  dvmptfsum  25139  ttgvalOLD  27237  msrfval  33499  poimirlem5  35782  poimirlem6  35783  poimirlem7  35784  poimirlem8  35785  poimirlem10  35787  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  poimirlem18  35795  poimirlem21  35798  poimirlem22  35799  poimirlem24  35801  poimirlem26  35803  poimirlem27  35804  cdleme31sde  38399  cdlemeg47rv2  38524  rnghmval  45449  dmmpossx2  45672