Theorem csbied2 3891

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ⦋csb 3854

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3747  df-csb 3855

This theorem is used by:  prdsval  17525  cidfval  17749  monfval  17806  idfuval  17950  isnat  18024  fucco  18039  catcval  18174  xpcval  18250  1stfval  18264  2ndfval  18267  prfval  18272  evlf2  18291  curfval  18296  hofval  18325  ipoval  18603  mntoval  33325  mgcoval  33329  erlval  33601  rlocval  33602  poimirlem2  38306  rngcvalALTV  49063  ringcvalALTV  49087  upfval  49987  swapfval  50073  fucofvalg  50129  fuco21  50147  prcofvalg  50187  lanfval  50424  ranfval  50425