Theorem csbied2 3911

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 2792	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵)
5		csbied2.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷)
6	4, 5	syldan 591	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷)
7	1, 6	csbied 3910	1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷)

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766  df-csb 3875

This theorem is referenced by:  prdsval  17469  cidfval  17688  monfval  17745  idfuval  17889  isnat  17963  fucco  17978  catcval  18113  xpcval  18189  1stfval  18203  2ndfval  18206  prfval  18211  evlf2  18230  curfval  18235  hofval  18264  ipoval  18540  mntoval  32962  mgcoval  32966  erlval  33253  rlocval  33254  poimirlem2  37646  rngcvalALTV  48240  ringcvalALTV  48264  upfval  49111  swapfval  49179  fucofvalg  49229  fuco21  49247  prcofvalg  49287  lanfval  49490  ranfval  49491