Theorem csbeq2dv 3857

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

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

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 3742  df-csb 3851

This theorem is referenced by:  csbeq2i  3858  csbeq12dv  3859  mpomptsx  8010  dmmpossx  8012  fmpox  8013  el2mpocsbcl  8029  offval22  8032  ovmptss  8037  fmpoco  8039  mposn  8047  mpocurryd  8213  fvmpocurryd  8215  cantnffval  9576  sumeq2sdv  15630  fsumcom2  15701  prodeq2sdv  15850  fprodcom2  15911  bpolylem  15975  bpolyval  15976  ruclem1  16160  natfval  17877  fucval  17889  evlfval  18144  rnghmval  20380  mpfrcl  22044  selvffval  22080  selvfval  22081  selvval  22082  pmatcollpw3lem  22731  fsumcn  24821  fsum2cn  24822  itgeq1f  25732  itgeq1  25734  dvmptfsum  25939  mulsval  28091  precsexlemcbv  28187  msrfval  35712  poimirlem5  37797  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem15  37807  poimirlem18  37810  poimirlem21  37813  poimirlem22  37814  poimirlem24  37816  poimirlem26  37818  poimirlem27  37819  cdleme31sde  40682  cdlemeg47rv2  40807  dmmpossx2  48619  dfswapf2  49542  fucofvalg  49599  dfinito4  49782