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. (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 2356 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbimi 1873 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | sbf 2368 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
7 | 6 | sblbis 2392 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
8 | 4, 7 | mpbi 219 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 Ⅎwnf 1699 [wsb 1867 |
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-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 |
This theorem is referenced by: sbied 2397 equsb3lem 2419 elsb3 2422 elsb4 2423 cbveu 2493 mo4f 2504 2mos 2540 eqsb3lem 2714 clelsb3 2716 cbvab 2733 cbvralf 3141 cbvreu 3145 sbralie 3160 cbvrab 3171 reu2 3361 nfcdeq 3399 sbcco2 3426 sbcie2g 3436 sbcralt 3477 sbcreu 3482 cbvralcsf 3531 cbvreucsf 3533 cbvrabcsf 3534 sbcel12 3935 sbceqg 3936 sbss 4034 sbcbr123 4636 cbvopab1 4655 cbvmpt 4677 wfis2fg 5634 cbviota 5773 cbvriota 6521 tfis2f 6947 tfinds 6951 nd1 9288 nd2 9289 clelsb3f 28704 rmo4fOLD 28720 rmo4f 28721 funcnv4mpt 28853 nn0min 28954 ballotlemodife 29886 bnj1321 30349 setinds2f 30928 frins2fg 30988 bj-clelsb3 32042 bj-sbeqALT 32087 prtlem5 33162 sbcrexgOLD 36367 sbcel12gOLD 37775 |
Copyright terms: Public domain | W3C validator |