Theorem csbied2 3868

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
csbied2.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
csbied2.2	⊢ (𝜑 → 𝐴 = 𝐵)
csbied2.3	⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
csbied2	⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝐷

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem csbied2

Step	Hyp	Ref	Expression
1		csbied2.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		id 22	. . . 4 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
3		csbied2.2	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	sylan9eqr 2801	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵)
5		csbied2.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)
6	4, 5	syldan 590	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)
7	1, 6	csbied 3866	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712  df-csb 3829

This theorem is referenced by:  prdsval  17083  cidfval  17302  monfval  17361  idfuval  17507  isnat  17579  fucco  17596  catcval  17731  xpcval  17810  1stfval  17824  2ndfval  17827  prfval  17832  evlf2  17852  curfval  17857  hofval  17886  ipoval  18163  mntoval  31162  mgcoval  31166  poimirlem2  35706  rngcvalALTV  45407  ringcvalALTV  45453