Theorem csbeq2dv 3853

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2738  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq2i  3854  csbeq12dv  3855  mpomptsx  8058  dmmpossx  8060  fmpox  8061  el2mpocsbcl  8079  offval22  8082  ovmptss  8087  fmpoco  8089  mposn  8097  mpocurryd  8264  fvmpocurryd  8266  cantnffval  9642  sumeq2sdv  15838  fsumcom2  15908  prodeq2sdv  16059  fprodcom2  16119  bpolylem  16182  bpolyval  16183  ruclem1  16367  natfval  18086  fucval  18098  evlfval  18353  rnghmval  20632  rhmval0  20667  mpfrcl  22356  selvffval  22389  selvfval  22390  selvval  22391  pmatcollpw3lem  23063  fsumcn  25153  fsum2cn  25154  itgeq1f  26054  itgeq1  26055  dvmptfsum  26257  mulsval  28429  precsexlemcbv  28526  msrfval  36223  nmulprop  36861  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem15  38473  poimirlem18  38476  poimirlem21  38479  poimirlem22  38480  poimirlem24  38482  poimirlem26  38484  poimirlem27  38485  cdleme31sde  41362  cdlemeg47rv2  41487  dmmpossx2  49371  dfswapf2  50291  fucofvalg  50348  dfinito4  50531