| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > csbied2 | Structured version Visualization version GIF version | ||
| Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| Ref | Expression |
|---|---|
| csbied2.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| csbied2.2 | ⊢ (𝜑 → 𝐴 = 𝐵) |
| csbied2.3 | ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) |
| Ref | Expression |
|---|---|
| csbied2 | ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | csbied2.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 2 | id 22 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) | |
| 3 | csbied2.2 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
| 4 | 2, 3 | sylan9eqr 2799 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) |
| 5 | csbied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) | |
| 6 | 4, 5 | syldan 591 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) |
| 7 | 1, 6 | csbied 3935 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ⦋csb 3899 |
| 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 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-sbc 3789 df-csb 3900 |
| This theorem is referenced by: prdsval 17500 cidfval 17719 monfval 17776 idfuval 17921 isnat 17995 fucco 18010 catcval 18145 xpcval 18222 1stfval 18236 2ndfval 18239 prfval 18244 evlf2 18263 curfval 18268 hofval 18297 ipoval 18575 mntoval 32972 mgcoval 32976 erlval 33262 rlocval 33263 poimirlem2 37629 rngcvalALTV 48181 ringcvalALTV 48205 upfval 48933 swapfval 48968 fucofvalg 49013 fuco21 49031 |
| Copyright terms: Public domain | W3C validator |