Theorem csbeq2dv 3853

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {cab 2738  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq2i  3854  csbeq12dv  3855  mpomptsx  8075  dmmpossx  8077  fmpox  8078  el2mpocsbcl  8096  offval22  8099  ovmptss  8104  fmpoco  8106  mposn  8114  mpocurryd  8287  fvmpocurryd  8289  cantnffval  9665  sumeq2sdv  15871  fsumcom2  15941  prodeq2sdv  16092  fprodcom2  16152  bpolylem  16215  bpolyval  16216  ruclem1  16400  natfval  18125  fucval  18137  evlfval  18392  rnghmval  20671  rhmval0  20706  mpfrcl  22395  selvffval  22428  selvfval  22429  selvval  22430  pmatcollpw3lem  23102  fsumcn  25192  fsum2cn  25193  itgeq1f  26093  itgeq1  26094  dvmptfsum  26296  mulsval  28496  precsexlemcbv  28593  msrfval  36371  nmulprop  37014  poimirlem5  38619  poimirlem6  38620  poimirlem7  38621  poimirlem8  38622  poimirlem10  38624  poimirlem11  38625  poimirlem12  38626  poimirlem15  38629  poimirlem18  38632  poimirlem21  38635  poimirlem22  38636  poimirlem24  38638  poimirlem26  38640  poimirlem27  38641  cdleme31sde  41518  cdlemeg47rv2  41643  dmmpossx2  49525  dfswapf2  50445  fucofvalg  50502  dfinito4  50685