Theorem csbeq2dv 3859

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  {cab 2739  [wsbc 3743  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744  df-csb 3853

This theorem is referenced by:  csbeq2i  3860  csbeq12dv  3861  mpomptsx  8060  dmmpossx  8062  fmpox  8063  el2mpocsbcl  8079  offval22  8082  ovmptss  8087  fmpoco  8089  mposn  8097  mpocurryd  8264  fvmpocurryd  8266  cantnffval  9631  sumeq2sdv  15754  fsumcom2  15825  prodeq2sdv  15977  fprodcom2  16038  bpolylem  16101  bpolyval  16102  ruclem1  16286  natfval  18005  fucval  18017  evlfval  18272  rnghmval  20521  mpfrcl  22215  selvffval  22248  selvfval  22249  selvval  22250  pmatcollpw3lem  22919  fsumcn  25008  fsum2cn  25009  itgeq1f  25909  itgeq1  25911  dvmptfsum  26113  mulsval  28278  precsexlemcbv  28375  msrfval  35995  nmulprop  36648  poimirlem5  38242  poimirlem6  38243  poimirlem7  38244  poimirlem8  38245  poimirlem10  38247  poimirlem11  38248  poimirlem12  38249  poimirlem15  38252  poimirlem18  38255  poimirlem21  38258  poimirlem22  38259  poimirlem24  38261  poimirlem26  38263  poimirlem27  38264  cdleme31sde  41127  cdlemeg47rv2  41252  dmmpossx2  49084  dfswapf2  50006  fucofvalg  50063  dfinito4  50246