Theorem csbeq2dv 3858

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3742  ⦋csb 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743  df-csb 3852

This theorem is referenced by:  csbeq2i  3859  csbeq12dv  3860  mpomptsx  8018  dmmpossx  8020  fmpox  8021  el2mpocsbcl  8037  offval22  8040  ovmptss  8045  fmpoco  8047  mposn  8055  mpocurryd  8221  fvmpocurryd  8223  cantnffval  9584  sumeq2sdv  15638  fsumcom2  15709  prodeq2sdv  15858  fprodcom2  15919  bpolylem  15983  bpolyval  15984  ruclem1  16168  natfval  17885  fucval  17897  evlfval  18152  rnghmval  20388  mpfrcl  22052  selvffval  22088  selvfval  22089  selvval  22090  pmatcollpw3lem  22739  fsumcn  24829  fsum2cn  24830  itgeq1f  25740  itgeq1  25742  dvmptfsum  25947  mulsval  28117  precsexlemcbv  28214  msrfval  35750  poimirlem5  37865  poimirlem6  37866  poimirlem7  37867  poimirlem8  37868  poimirlem10  37870  poimirlem11  37871  poimirlem12  37872  poimirlem15  37875  poimirlem18  37878  poimirlem21  37881  poimirlem22  37882  poimirlem24  37884  poimirlem26  37886  poimirlem27  37887  cdleme31sde  40750  cdlemeg47rv2  40875  dmmpossx2  48686  dfswapf2  49609  fucofvalg  49666  dfinito4  49849