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 2666 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) |
5 | csbied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) | |
6 | 4, 5 | syldan 486 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) |
7 | 1, 6 | csbied 3526 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: prdsval 15938 cidfval 16160 monfval 16215 idfuval 16359 isnat 16430 fucco 16445 catcval 16569 xpcval 16640 1stfval 16654 2ndfval 16657 prfval 16662 evlf2 16681 curfval 16686 hofval 16715 ipoval 16977 poimirlem2 32581 rngcvalALTV 41753 ringcvalALTV 41799 |
Copyright terms: Public domain | W3C validator |