![]() |
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 versions requiring disjoint variables, but fewer axioms, see sbiev 2311 and sbievw 2089. Usage of this theorem is discouraged because it depends on ax-13 2373. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sbie.1 | ⊢ Ⅎ𝑥𝜓 |
sbie.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
sbie | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equsb1 2492 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | sbimi 2070 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
6 | 5 | sbf 2267 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
7 | 6 | sblbis 2306 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
8 | 4, 7 | mpbi 230 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1778 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-10 2137 ax-12 2173 ax-13 2373 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-ex 1775 df-nf 1779 df-sb 2061 |
This theorem is referenced by: sbied 2504 2sbiev 2506 cbvmo 2600 cbveu 2603 cbvab 2810 clelsb2OLD 2866 cbvralf 3356 cbvreu 3424 cbvrab 3476 nfcdeq 3786 cbvralcsf 3953 cbvreucsf 3955 cbvrabcsf 3956 cbvopab1g 5226 cbvmptfg 5260 cbviota 6521 cbvriota 7396 nd1 10619 nd2 10620 sbcrexgOLD 42734 |
Copyright terms: Public domain | W3C validator |