Theorem csbeq2dv 3869

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  [wsbc 3753  ⦋csb 3862

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbeq2i  3870  csbeq12dv  3871  mpomptsx  8043  dmmpossx  8045  fmpox  8046  el2mpocsbcl  8064  offval22  8067  ovmptss  8072  fmpoco  8074  mposn  8082  mpocurryd  8248  fvmpocurryd  8250  cantnffval  9616  sumeq2sdv  15669  fsumcom2  15740  prodeq2sdv  15889  fprodcom2  15950  bpolylem  16014  bpolyval  16015  ruclem1  16199  natfval  17911  fucval  17923  evlfval  18178  rnghmval  20349  mpfrcl  21992  selvffval  22020  selvfval  22021  selvval  22022  pmatcollpw3lem  22670  fsumcn  24761  fsum2cn  24762  itgeq1f  25672  itgeq1  25674  dvmptfsum  25879  mulsval  28012  precsexlemcbv  28108  msrfval  35524  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem24  37638  poimirlem26  37640  poimirlem27  37641  cdleme31sde  40379  cdlemeg47rv2  40504  dmmpossx2  48325  dfswapf2  49250  fucofvalg  49307  dfinito4  49490