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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  {cab 2734  [wsbc 3739  ⦋csb 3847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-sbc 3740  df-csb 3848

This theorem is referenced by:  csbeq2i  3855  csbeq12dv  3856  mpomptsx  8034  dmmpossx  8036  fmpox  8037  el2mpocsbcl  8052  offval22  8055  ovmptss  8060  fmpoco  8062  mposn  8070  mpocurryd  8237  fvmpocurryd  8239  cantnffval  9608  sumeq2sdv  15706  fsumcom2  15777  prodeq2sdv  15929  fprodcom2  15990  bpolylem  16054  bpolyval  16055  ruclem1  16239  natfval  17958  fucval  17970  evlfval  18225  rnghmval  20461  mpfrcl  22111  selvffval  22144  selvfval  22145  selvval  22146  pmatcollpw3lem  22816  fsumcn  24905  fsum2cn  24906  itgeq1f  25806  itgeq1  25808  dvmptfsum  26010  mulsval  28172  precsexlemcbv  28269  msrfval  35835  nmulprop  36488  poimirlem5  38072  poimirlem6  38073  poimirlem7  38074  poimirlem8  38075  poimirlem10  38077  poimirlem11  38078  poimirlem12  38079  poimirlem15  38082  poimirlem18  38085  poimirlem21  38088  poimirlem22  38089  poimirlem24  38091  poimirlem26  38093  poimirlem27  38094  cdleme31sde  40957  cdlemeg47rv2  41082  dmmpossx2  48907  dfswapf2  49830  fucofvalg  49887  dfinito4  50070