![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbie | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution. For a version requiring disjoint variables, but fewer axioms, see sbiev 2345. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) |
Ref | Expression |
---|---|
sbie.1 | ⊢ Ⅎ𝑥𝜓 |
sbie.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbie | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsb1 2500 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbimi 2075 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | sbf 2512 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
7 | 6 | sblbis 2536 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
8 | 4, 7 | mpbi 222 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 Ⅎwnf 1884 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-10 2194 ax-12 2222 ax-13 2391 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-ex 1881 df-nf 1885 df-sb 2070 |
This theorem is referenced by: sbied 2541 equsb3vOLD 2565 elsb3OLD 2570 elsb4OLD 2573 mo4fOLD 2638 cbvmo 2691 cbveu 2692 2mos 2733 eqsb3lem 2933 clelsb3 2935 cbvab 2952 clelsb3f 2974 cbvralf 3378 cbvreu 3382 sbralie 3397 cbvrab 3412 reu2 3620 rmo4f 3630 nfcdeq 3660 sbcco2 3687 sbcie2g 3697 sbcralt 3736 sbcreu 3740 cbvralcsf 3790 cbvreucsf 3792 cbvrabcsf 3793 sbcel12 4208 sbceqg 4209 sbss 4305 sbcbr123 4928 cbvopab1 4947 cbvmpt 4973 wfis2fg 5958 cbviota 6092 cbvriota 6877 tfis2f 7317 tfinds 7321 nd1 9725 nd2 9726 clwwlknonclwlknonf1o 27761 clwwlknonclwlknonf1oOLD 27762 dlwwlknondlwlknonf1o 27767 dlwwlknondlwlknonf1oOLD 27768 funcnv4mpt 30019 nn0min 30115 ballotlemodife 31106 bnj1321 31642 setinds2f 32223 frins2fg 32287 bj-sbeqALT 33417 prtlem5 34936 sbcrexgOLD 38194 |
Copyright terms: Public domain | W3C validator |