Theorem csbeq2dv 3896

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

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

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 3774  df-csb 3890

This theorem is referenced by:  csbeq2i  3897  csbeq12dv  3898  mpomptsx  8069  dmmpossx  8071  fmpox  8072  el2mpocsbcl  8090  offval22  8093  ovmptss  8098  fmpoco  8100  mposn  8108  mpocurryd  8275  fvmpocurryd  8277  cantnffval  9688  fsumcom2  15756  fprodcom2  15964  bpolylem  16028  bpolyval  16029  ruclem1  16211  natfval  17939  fucval  17952  evlfval  18212  rnghmval  20391  mpfrcl  22053  selvffval  22081  selvfval  22082  selvval  22083  pmatcollpw3lem  22729  fsumcn  24832  fsum2cn  24833  dvmptfsum  25951  mulsval  28059  precsexlemcbv  28154  ttgvalOLD  28752  msrfval  35278  poimirlem5  37229  poimirlem6  37230  poimirlem7  37231  poimirlem8  37232  poimirlem10  37234  poimirlem11  37235  poimirlem12  37236  poimirlem15  37239  poimirlem18  37242  poimirlem21  37245  poimirlem22  37246  poimirlem24  37248  poimirlem26  37250  poimirlem27  37251  cdleme31sde  39988  cdlemeg47rv2  40113  dmmpossx2  47586