![]() |
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 2396 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbimi 1943 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | sbf 2408 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
7 | 6 | sblbis 2432 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
8 | 4, 7 | mpbi 220 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 Ⅎwnf 1748 [wsb 1937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 df-sb 1938 |
This theorem is referenced by: sbied 2437 equsb3lem 2459 elsb3 2462 elsb4 2463 cbveu 2534 mo4f 2545 2mos 2581 eqsb3lem 2756 clelsb3 2758 cbvab 2775 clelsb3f 2797 cbvralf 3195 cbvreu 3199 sbralie 3214 cbvrab 3229 reu2 3427 nfcdeq 3465 sbcco2 3492 sbcie2g 3502 sbcralt 3543 sbcreu 3548 cbvralcsf 3598 cbvreucsf 3600 cbvrabcsf 3601 sbcel12 4016 sbceqg 4017 sbss 4117 sbcbr123 4739 cbvopab1 4756 cbvmpt 4782 wfis2fg 5755 cbviota 5894 cbvriota 6661 tfis2f 7097 tfinds 7101 nd1 9447 nd2 9448 rmo4fOLD 29463 rmo4f 29464 funcnv4mpt 29598 nn0min 29695 ballotlemodife 30687 bnj1321 31221 setinds2f 31808 frins2fg 31872 bj-clelsb3 32973 bj-sbeqALT 33020 prtlem5 34464 sbcrexgOLD 37666 sbcel12gOLD 39071 |
Copyright terms: Public domain | W3C validator |