![]() |
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 2286. (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 2444 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbimi 2017 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | sbf 2456 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
7 | 6 | sblbis 2480 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
8 | 4, 7 | mpbi 222 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 Ⅎwnf 1827 [wsb 2011 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-10 2135 ax-12 2163 ax-13 2334 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-ex 1824 df-nf 1828 df-sb 2012 |
This theorem is referenced by: sbied 2485 equsb3vOLD 2509 elsb3OLD 2514 elsb4OLD 2517 mo4fOLD 2584 cbvmo 2637 cbveu 2638 2mos 2679 eqsb3vOLD 2886 clelsb3 2888 cbvab 2913 clelsb3fOLD 2939 cbvralf 3361 cbvreu 3365 sbralie 3380 cbvrab 3395 reu2 3606 rmo4f 3616 nfcdeq 3649 sbcco2 3676 sbcie2g 3686 sbcralt 3728 sbcreu 3732 cbvralcsf 3783 cbvreucsf 3785 cbvrabcsf 3786 sbcel12 4208 sbceqg 4209 sbss 4305 sbcbr123 4942 cbvopab1 4961 cbvmpt 4986 wfis2fg 5972 cbviota 6106 cbvriota 6895 tfis2f 7335 tfinds 7339 nd1 9746 nd2 9747 clwwlknonclwlknonf1o 27789 clwwlknonclwlknonf1oOLD 27790 dlwwlknondlwlknonf1o 27795 dlwwlknondlwlknonf1oOLD 27796 funcnv4mpt 30038 nn0min 30135 ballotlemodife 31162 bnj1321 31698 setinds2f 32276 frins2fg 32340 bj-sbeqALT 33470 prtlem5 35019 sbcrexgOLD 38319 2reu8i 42164 |
Copyright terms: Public domain | W3C validator |