Theorem csbeq2dv 3868

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {cab 2747  [wsbc 3753  ⦋csb 3861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754  df-csb 3862

This theorem is referenced by:  csbeq2i  3869  csbeq12dv  3870  mpomptsx  8060  dmmpossx  8062  fmpox  8063  el2mpocsbcl  8079  offval22  8082  ovmptss  8087  fmpoco  8089  mposn  8097  mpocurryd  8264  fvmpocurryd  8266  cantnffval  9631  sumeq2sdv  15753  fsumcom2  15824  prodeq2sdv  15976  fprodcom2  16037  bpolylem  16101  bpolyval  16102  ruclem1  16286  natfval  18005  fucval  18017  evlfval  18272  rnghmval  20521  mpfrcl  22204  selvffval  22237  selvfval  22238  selvval  22239  pmatcollpw3lem  22908  fsumcn  24997  fsum2cn  24998  itgeq1f  25898  itgeq1  25900  dvmptfsum  26102  mulsval  28267  precsexlemcbv  28364  msrfval  35927  nmulprop  36580  poimirlem5  38163  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem10  38168  poimirlem11  38169  poimirlem12  38170  poimirlem15  38173  poimirlem18  38176  poimirlem21  38179  poimirlem22  38180  poimirlem24  38182  poimirlem26  38184  poimirlem27  38185  cdleme31sde  41048  cdlemeg47rv2  41173  dmmpossx2  49001  dfswapf2  49923  fucofvalg  49980  dfinito4  50163