Theorem csbied2 3818

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ⦋csb 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-v 3417  df-sbc 3684  df-csb 3789

This theorem is referenced by:  prdsval  16587  cidfval  16808  monfval  16863  idfuval  17007  isnat  17078  fucco  17093  catcval  17217  xpcval  17288  1stfval  17302  2ndfval  17305  prfval  17310  evlf2  17329  curfval  17334  hofval  17363  ipoval  17625  poimirlem2  34335  rngcvalALTV  43597  ringcvalALTV  43643