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 2875 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵) |
5 | csbied2.3 | . . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → 𝐶 = 𝐷) | |
6 | 4, 5 | syldan 591 | . 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐶 = 𝐷) |
7 | 1, 6 | csbied 3916 | 1 ⊢ (𝜑 → ⦋𝐴 / 𝑥⦌𝐶 = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 ⦋csb 3880 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-sbc 3770 df-csb 3881 |
This theorem is referenced by: prdsval 16716 cidfval 16935 monfval 16990 idfuval 17134 isnat 17205 fucco 17220 catcval 17344 xpcval 17415 1stfval 17429 2ndfval 17432 prfval 17437 evlf2 17456 curfval 17461 hofval 17490 ipoval 17752 poimirlem2 34775 rngcvalALTV 44160 ringcvalALTV 44206 |
Copyright terms: Public domain | W3C validator |