Theorem csbeq2dv 3857

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2740  [wsbc 3742  ⦋csb 3850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbeq2i  3858  csbeq12dv  3859  mpomptsx  8064  dmmpossx  8066  fmpox  8067  el2mpocsbcl  8085  offval22  8088  ovmptss  8093  fmpoco  8095  mposn  8103  mpocurryd  8270  fvmpocurryd  8272  cantnffval  9645  sumeq2sdv  15792  fsumcom2  15862  prodeq2sdv  16014  fprodcom2  16075  bpolylem  16138  bpolyval  16139  ruclem1  16323  natfval  18042  fucval  18054  evlfval  18309  rnghmval  20585  rhmval0  20620  mpfrcl  22305  selvffval  22338  selvfval  22339  selvval  22340  pmatcollpw3lem  23012  fsumcn  25102  fsum2cn  25103  itgeq1f  26003  itgeq1  26005  dvmptfsum  26207  mulsval  28375  precsexlemcbv  28472  msrfval  36118  nmulprop  36772  poimirlem5  38376  poimirlem6  38377  poimirlem7  38378  poimirlem8  38379  poimirlem10  38381  poimirlem11  38382  poimirlem12  38383  poimirlem15  38386  poimirlem18  38389  poimirlem21  38392  poimirlem22  38393  poimirlem24  38395  poimirlem26  38397  poimirlem27  38398  cdleme31sde  41260  cdlemeg47rv2  41385  dmmpossx2  49269  dfswapf2  50189  fucofvalg  50246  dfinito4  50429