Theorem csbeq2dv 3862

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748  df-csb 3856

This theorem is referenced by:  csbeq2i  3863  csbeq12dv  3864  mpomptsx  8049  dmmpossx  8051  fmpox  8052  el2mpocsbcl  8068  offval22  8071  ovmptss  8076  fmpoco  8078  mposn  8086  mpocurryd  8253  fvmpocurryd  8255  cantnffval  9620  sumeq2sdv  15744  fsumcom2  15815  prodeq2sdv  15967  fprodcom2  16028  bpolylem  16092  bpolyval  16093  ruclem1  16277  natfval  17996  fucval  18008  evlfval  18263  rnghmval  20513  mpfrcl  22196  selvffval  22229  selvfval  22230  selvval  22231  pmatcollpw3lem  22901  fsumcn  24990  fsum2cn  24991  itgeq1f  25891  itgeq1  25893  dvmptfsum  26095  mulsval  28260  precsexlemcbv  28357  msrfval  35900  nmulprop  36553  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem15  38146  poimirlem18  38149  poimirlem21  38152  poimirlem22  38153  poimirlem24  38155  poimirlem26  38157  poimirlem27  38158  cdleme31sde  41021  cdlemeg47rv2  41146  dmmpossx2  48968  dfswapf2  49890  fucofvalg  49947  dfinito4  50130