Theorem csbeq2dv 3855

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  {cab 2708  [wsbc 3739  ⦋csb 3848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3740  df-csb 3849

This theorem is referenced by:  csbeq2i  3856  csbeq12dv  3857  mpomptsx  7991  dmmpossx  7993  fmpox  7994  el2mpocsbcl  8010  offval22  8013  ovmptss  8018  fmpoco  8020  mposn  8028  mpocurryd  8194  fvmpocurryd  8196  cantnffval  9548  sumeq2sdv  15602  fsumcom2  15673  prodeq2sdv  15822  fprodcom2  15883  bpolylem  15947  bpolyval  15948  ruclem1  16132  natfval  17848  fucval  17860  evlfval  18115  rnghmval  20351  mpfrcl  22013  selvffval  22041  selvfval  22042  selvval  22043  pmatcollpw3lem  22691  fsumcn  24781  fsum2cn  24782  itgeq1f  25692  itgeq1  25694  dvmptfsum  25899  mulsval  28041  precsexlemcbv  28137  msrfval  35549  poimirlem5  37644  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem15  37654  poimirlem18  37657  poimirlem21  37660  poimirlem22  37661  poimirlem24  37663  poimirlem26  37665  poimirlem27  37666  cdleme31sde  40403  cdlemeg47rv2  40528  dmmpossx2  48347  dfswapf2  49272  fucofvalg  49329  dfinito4  49512