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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {cab 2718  [wsbc 3730  ⦋csb 3838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sbc 3731  df-csb 3839

This theorem is referenced by:  csbeq2i  3846  csbeq12dv  3847  mpomptsx  8013  dmmpossx  8015  fmpox  8016  el2mpocsbcl  8031  offval22  8034  ovmptss  8039  fmpoco  8041  mposn  8049  mpocurryd  8216  fvmpocurryd  8218  cantnffval  9582  sumeq2sdv  15663  fsumcom2  15734  prodeq2sdv  15886  fprodcom2  15947  bpolylem  16011  bpolyval  16012  ruclem1  16196  natfval  17914  fucval  17926  evlfval  18181  rnghmval  20418  mpfrcl  22068  selvffval  22101  selvfval  22102  selvval  22103  pmatcollpw3lem  22773  fsumcn  24862  fsum2cn  24863  itgeq1f  25763  itgeq1  25765  dvmptfsum  25967  mulsval  28126  precsexlemcbv  28223  msrfval  35766  poimirlem5  37993  poimirlem6  37994  poimirlem7  37995  poimirlem8  37996  poimirlem10  37998  poimirlem11  37999  poimirlem12  38000  poimirlem15  38003  poimirlem18  38006  poimirlem21  38009  poimirlem22  38010  poimirlem24  38012  poimirlem26  38014  poimirlem27  38015  cdleme31sde  40878  cdlemeg47rv2  41003  dmmpossx2  48829  dfswapf2  49752  fucofvalg  49809  dfinito4  49992