Theorem csbeq2dv 3969

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

Syntax hints:   → wi 4   = wceq 1480  ⦋csb 3519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-sbc 3423  df-csb 3520

This theorem is referenced by:  csbeq2i  3970  mpt2mptsx  7179  dmmpt2ssx  7181  fmpt2x  7182  el2mpt2csbcl  7196  offval22  7199  ovmptss  7204  fmpt2co  7206  mpt2sn  7214  mpt2curryd  7341  fvmpt2curryd  7343  cantnffval  8505  fsumcom2  14428  fsumcom2OLD  14429  fprodcom2  14634  fprodcom2OLD  14635  bpolylem  14699  bpolyval  14700  ruclem1  14880  natfval  16522  fucval  16534  evlfval  16773  mpfrcl  19432  pmatcollpw3lem  20502  fsumcn  22576  fsum2cn  22577  dvmptfsum  23637  ttgval  25650  msrfval  31134  poimirlem5  33032  poimirlem6  33033  poimirlem7  33034  poimirlem8  33035  poimirlem10  33037  poimirlem11  33038  poimirlem12  33039  poimirlem15  33042  poimirlem16  33043  poimirlem17  33044  poimirlem18  33045  poimirlem19  33046  poimirlem20  33047  poimirlem21  33048  poimirlem22  33049  poimirlem24  33051  poimirlem26  33053  poimirlem27  33054  cdleme31sde  35139  cdlemeg47rv2  35264  rnghmval  41152  dmmpt2ssx2  41376