Theorem csbeq2dv 3854

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {cab 2711  [wsbc 3738  ⦋csb 3847

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3739  df-csb 3848

This theorem is referenced by:  csbeq2i  3855  csbeq12dv  3856  mpomptsx  8005  dmmpossx  8007  fmpox  8008  el2mpocsbcl  8024  offval22  8027  ovmptss  8032  fmpoco  8034  mposn  8042  mpocurryd  8208  fvmpocurryd  8210  cantnffval  9563  sumeq2sdv  15620  fsumcom2  15691  prodeq2sdv  15840  fprodcom2  15901  bpolylem  15965  bpolyval  15966  ruclem1  16150  natfval  17866  fucval  17878  evlfval  18133  rnghmval  20368  mpfrcl  22030  selvffval  22058  selvfval  22059  selvval  22060  pmatcollpw3lem  22708  fsumcn  24798  fsum2cn  24799  itgeq1f  25709  itgeq1  25711  dvmptfsum  25916  mulsval  28058  precsexlemcbv  28154  msrfval  35592  poimirlem5  37675  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem15  37685  poimirlem18  37688  poimirlem21  37691  poimirlem22  37692  poimirlem24  37694  poimirlem26  37696  poimirlem27  37697  cdleme31sde  40494  cdlemeg47rv2  40619  dmmpossx2  48451  dfswapf2  49376  fucofvalg  49433  dfinito4  49616