Theorem csbeq2dv 3906

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

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		csbeq2dv.1	. . . . 5 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	eleq2d 2827	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
3	2	sbcbidv 3845	. . 3 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
4	3	abbidv 2808	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
5		df-csb 3900	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		df-csb 3900	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
7	4, 5, 6	3eqtr4g 2802	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2714  [wsbc 3788  ⦋csb 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789  df-csb 3900

This theorem is referenced by:  csbeq2i  3907  csbeq12dv  3908  mpomptsx  8089  dmmpossx  8091  fmpox  8092  el2mpocsbcl  8110  offval22  8113  ovmptss  8118  fmpoco  8120  mposn  8128  mpocurryd  8294  fvmpocurryd  8296  cantnffval  9703  sumeq2sdv  15739  fsumcom2  15810  prodeq2sdv  15959  fprodcom2  16020  bpolylem  16084  bpolyval  16085  ruclem1  16267  natfval  17994  fucval  18006  evlfval  18262  rnghmval  20440  mpfrcl  22109  selvffval  22137  selvfval  22138  selvval  22139  pmatcollpw3lem  22789  fsumcn  24894  fsum2cn  24895  itgeq1f  25806  itgeq1  25808  dvmptfsum  26013  mulsval  28135  precsexlemcbv  28230  ttgvalOLD  28884  msrfval  35542  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  poimirlem26  37653  poimirlem27  37654  cdleme31sde  40387  cdlemeg47rv2  40512  dmmpossx2  48253  dfswapf2  48967  fucofvalg  49013