Theorem csbeq2dv 3892

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

Syntax hints:   → wi 4   = wceq 1537  ⦋csb 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775  df-csb 3886

This theorem is referenced by:  csbeq2i  3893  csbeq12dv  3894  mpomptsx  7764  dmmpossx  7766  fmpox  7767  el2mpocsbcl  7782  offval22  7785  ovmptss  7790  fmpoco  7792  mposn  7800  mpocurryd  7937  fvmpocurryd  7939  cantnffval  9128  fsumcom2  15131  fprodcom2  15340  bpolylem  15404  bpolyval  15405  ruclem1  15586  natfval  17218  fucval  17230  evlfval  17469  mpfrcl  20300  selvffval  20331  selvfval  20332  selvval  20333  pmatcollpw3lem  21393  fsumcn  23480  fsum2cn  23481  dvmptfsum  24574  ttgval  26663  msrfval  32786  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem24  34918  poimirlem26  34920  poimirlem27  34921  cdleme31sde  37523  cdlemeg47rv2  37648  rnghmval  44169  dmmpossx2  44392