Theorem csbeq2dv 3858

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

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

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 3743  df-csb 3852

This theorem is referenced by:  csbeq2i  3859  csbeq12dv  3860  mpomptsx  7999  dmmpossx  8001  fmpox  8002  el2mpocsbcl  8018  offval22  8021  ovmptss  8026  fmpoco  8028  mposn  8036  mpocurryd  8202  fvmpocurryd  8204  cantnffval  9559  sumeq2sdv  15610  fsumcom2  15681  prodeq2sdv  15830  fprodcom2  15891  bpolylem  15955  bpolyval  15956  ruclem1  16140  natfval  17856  fucval  17868  evlfval  18123  rnghmval  20325  mpfrcl  21990  selvffval  22018  selvfval  22019  selvval  22020  pmatcollpw3lem  22668  fsumcn  24759  fsum2cn  24760  itgeq1f  25670  itgeq1  25672  dvmptfsum  25877  mulsval  28017  precsexlemcbv  28113  msrfval  35520  poimirlem5  37615  poimirlem6  37616  poimirlem7  37617  poimirlem8  37618  poimirlem10  37620  poimirlem11  37621  poimirlem12  37622  poimirlem15  37625  poimirlem18  37628  poimirlem21  37631  poimirlem22  37632  poimirlem24  37634  poimirlem26  37636  poimirlem27  37637  cdleme31sde  40374  cdlemeg47rv2  40499  dmmpossx2  48331  dfswapf2  49256  fucofvalg  49313  dfinito4  49496