Theorem csbeq2dv 3845

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 2823	. . . 4 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶))
3	2	sbcbidv 3785	. . 3 ⊢ (𝜑 → ([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ [𝐴 / 𝑥]𝑦 ∈ 𝐶))
4	3	abbidv 2803	. 2 ⊢ (𝜑 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶})
5		df-csb 3839	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
6		df-csb 3839	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
7	4, 5, 6	3eqtr4g 2797	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3729  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730  df-csb 3839

This theorem is referenced by:  csbeq2i  3846  csbeq12dv  3847  mpomptsx  8008  dmmpossx  8010  fmpox  8011  el2mpocsbcl  8026  offval22  8029  ovmptss  8034  fmpoco  8036  mposn  8044  mpocurryd  8210  fvmpocurryd  8212  cantnffval  9573  sumeq2sdv  15654  fsumcom2  15725  prodeq2sdv  15877  fprodcom2  15938  bpolylem  16002  bpolyval  16003  ruclem1  16187  natfval  17905  fucval  17917  evlfval  18172  rnghmval  20409  mpfrcl  22072  selvffval  22108  selvfval  22109  selvval  22110  pmatcollpw3lem  22757  fsumcn  24846  fsum2cn  24847  itgeq1f  25747  itgeq1  25749  dvmptfsum  25951  mulsval  28120  precsexlemcbv  28217  msrfval  35740  poimirlem5  37957  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem10  37962  poimirlem11  37963  poimirlem12  37964  poimirlem15  37967  poimirlem18  37970  poimirlem21  37973  poimirlem22  37974  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  cdleme31sde  40842  cdlemeg47rv2  40967  dmmpossx2  48810  dfswapf2  49733  fucofvalg  49790  dfinito4  49973