Theorem csbeq2dv 3860

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  [wsbc 3744  ⦋csb 3853

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745  df-csb 3854

This theorem is referenced by:  csbeq2i  3861  csbeq12dv  3862  mpomptsx  8006  dmmpossx  8008  fmpox  8009  el2mpocsbcl  8025  offval22  8028  ovmptss  8033  fmpoco  8035  mposn  8043  mpocurryd  8209  fvmpocurryd  8211  cantnffval  9578  sumeq2sdv  15628  fsumcom2  15699  prodeq2sdv  15848  fprodcom2  15909  bpolylem  15973  bpolyval  15974  ruclem1  16158  natfval  17874  fucval  17886  evlfval  18141  rnghmval  20343  mpfrcl  22008  selvffval  22036  selvfval  22037  selvval  22038  pmatcollpw3lem  22686  fsumcn  24777  fsum2cn  24778  itgeq1f  25688  itgeq1  25690  dvmptfsum  25895  mulsval  28035  precsexlemcbv  28131  msrfval  35509  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem15  37614  poimirlem18  37617  poimirlem21  37620  poimirlem22  37621  poimirlem24  37623  poimirlem26  37625  poimirlem27  37626  cdleme31sde  40364  cdlemeg47rv2  40489  dmmpossx2  48309  dfswapf2  49234  fucofvalg  49291  dfinito4  49474