Theorem csbeq2dv 3871

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2708  [wsbc 3755  ⦋csb 3864

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3756  df-csb 3865

This theorem is referenced by:  csbeq2i  3872  csbeq12dv  3873  mpomptsx  8045  dmmpossx  8047  fmpox  8048  el2mpocsbcl  8066  offval22  8069  ovmptss  8074  fmpoco  8076  mposn  8084  mpocurryd  8250  fvmpocurryd  8252  cantnffval  9622  sumeq2sdv  15675  fsumcom2  15746  prodeq2sdv  15895  fprodcom2  15956  bpolylem  16020  bpolyval  16021  ruclem1  16205  natfval  17917  fucval  17929  evlfval  18184  rnghmval  20355  mpfrcl  21998  selvffval  22026  selvfval  22027  selvval  22028  pmatcollpw3lem  22676  fsumcn  24767  fsum2cn  24768  itgeq1f  25678  itgeq1  25680  dvmptfsum  25885  mulsval  28018  precsexlemcbv  28114  msrfval  35524  poimirlem5  37614  poimirlem6  37615  poimirlem7  37616  poimirlem8  37617  poimirlem10  37619  poimirlem11  37620  poimirlem12  37621  poimirlem15  37624  poimirlem18  37627  poimirlem21  37630  poimirlem22  37631  poimirlem24  37633  poimirlem26  37635  poimirlem27  37636  cdleme31sde  40374  cdlemeg47rv2  40499  dmmpossx2  48315  dfswapf2  49240  fucofvalg  49297  dfinito4  49480