Theorem csbeq2dv 3886

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2714  [wsbc 3770  ⦋csb 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-sbc 3771  df-csb 3880

This theorem is referenced by:  csbeq2i  3887  csbeq12dv  3888  mpomptsx  8068  dmmpossx  8070  fmpox  8071  el2mpocsbcl  8089  offval22  8092  ovmptss  8097  fmpoco  8099  mposn  8107  mpocurryd  8273  fvmpocurryd  8275  cantnffval  9682  sumeq2sdv  15724  fsumcom2  15795  prodeq2sdv  15944  fprodcom2  16005  bpolylem  16069  bpolyval  16070  ruclem1  16254  natfval  17967  fucval  17979  evlfval  18234  rnghmval  20405  mpfrcl  22048  selvffval  22076  selvfval  22077  selvval  22078  pmatcollpw3lem  22726  fsumcn  24817  fsum2cn  24818  itgeq1f  25729  itgeq1  25731  dvmptfsum  25936  mulsval  28069  precsexlemcbv  28165  msrfval  35564  poimirlem5  37654  poimirlem6  37655  poimirlem7  37656  poimirlem8  37657  poimirlem10  37659  poimirlem11  37660  poimirlem12  37661  poimirlem15  37664  poimirlem18  37667  poimirlem21  37670  poimirlem22  37671  poimirlem24  37673  poimirlem26  37675  poimirlem27  37676  cdleme31sde  40409  cdlemeg47rv2  40534  dmmpossx2  48279  dfswapf2  49145  fucofvalg  49196  dfinito4  49353