Theorem csbeq2dv 3890

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

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

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3773  df-csb 3884

This theorem is referenced by:  csbeq2i  3891  csbeq12dv  3892  mpomptsx  7762  dmmpossx  7764  fmpox  7765  el2mpocsbcl  7780  offval22  7783  ovmptss  7788  fmpoco  7790  mposn  7798  mpocurryd  7935  fvmpocurryd  7937  cantnffval  9126  fsumcom2  15129  fprodcom2  15338  bpolylem  15402  bpolyval  15403  ruclem1  15584  natfval  17216  fucval  17228  evlfval  17467  mpfrcl  20298  selvffval  20329  selvfval  20330  selvval  20331  pmatcollpw3lem  21391  fsumcn  23478  fsum2cn  23479  dvmptfsum  24572  ttgval  26661  msrfval  32784  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  cdleme31sde  37536  cdlemeg47rv2  37661  rnghmval  44182  dmmpossx2  44405