Theorem csbeq2dv 4135

Description: Formula-building deduction rule 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 1992	. 2 ⊢ Ⅎ𝑥𝜑
2		csbeq2dv.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	csbeq2d 4134	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1632  ⦋csb 3674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-sbc 3577  df-csb 3675

This theorem is referenced by:  csbeq2i  4136  mpt2mptsx  7401  dmmpt2ssx  7403  fmpt2x  7404  el2mpt2csbcl  7418  offval22  7421  ovmptss  7426  fmpt2co  7428  mpt2sn  7436  mpt2curryd  7564  fvmpt2curryd  7566  cantnffval  8733  fsumcom2  14704  fsumcom2OLD  14705  fprodcom2  14913  fprodcom2OLD  14914  bpolylem  14978  bpolyval  14979  ruclem1  15159  natfval  16807  fucval  16819  evlfval  17058  mpfrcl  19720  pmatcollpw3lem  20790  fsumcn  22874  fsum2cn  22875  dvmptfsum  23937  ttgval  25954  msrfval  31741  poimirlem5  33727  poimirlem6  33728  poimirlem7  33729  poimirlem8  33730  poimirlem10  33732  poimirlem11  33733  poimirlem12  33734  poimirlem15  33737  poimirlem16  33738  poimirlem17  33739  poimirlem18  33740  poimirlem19  33741  poimirlem20  33742  poimirlem21  33743  poimirlem22  33744  poimirlem24  33746  poimirlem26  33748  poimirlem27  33749  cdleme31sde  36175  cdlemeg47rv2  36300  rnghmval  42401  dmmpt2ssx2  42625