Theorem csbied2 3838

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ⦋csb 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-sbc 3684  df-csb 3799

This theorem is referenced by:  prdsval  16914  cidfval  17133  monfval  17191  idfuval  17336  isnat  17408  fucco  17425  catcval  17560  xpcval  17638  1stfval  17652  2ndfval  17655  prfval  17660  evlf2  17680  curfval  17685  hofval  17714  ipoval  17990  mntoval  30933  mgcoval  30937  poimirlem2  35465  rngcvalALTV  45135  ringcvalALTV  45181