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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  {cab 2740  [wsbc 3743  ⦋csb 3852

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3744  df-csb 3853

This theorem is used by:  csbeq2i  3860  csbeq12dv  3861  mpomptsx  8059  dmmpossx  8061  fmpox  8062  el2mpocsbcl  8078  offval22  8081  ovmptss  8086  fmpoco  8088  mposn  8096  mpocurryd  8263  fvmpocurryd  8265  cantnffval  9630  sumeq2sdv  15761  fsumcom2  15832  prodeq2sdv  15984  fprodcom2  16045  bpolylem  16108  bpolyval  16109  ruclem1  16293  natfval  18012  fucval  18024  evlfval  18279  rnghmval  20529  rhmval0  20564  mpfrcl  22247  selvffval  22280  selvfval  22281  selvval  22282  pmatcollpw3lem  22951  fsumcn  25040  fsum2cn  25041  itgeq1f  25941  itgeq1  25943  dvmptfsum  26145  mulsval  28313  precsexlemcbv  28410  msrfval  36037  nmulprop  36690  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem15  38314  poimirlem18  38317  poimirlem21  38320  poimirlem22  38321  poimirlem24  38323  poimirlem26  38325  poimirlem27  38326  cdleme31sde  41187  cdlemeg47rv2  41312  dmmpossx2  49145  dfswapf2  50067  fucofvalg  50124  dfinito4  50307