| 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 2314 and sbievw 2093. Usage of this theorem is discouraged because it depends on ax-13 2376. (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 2495 | . . 3 ⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | |
| 2 | sbie.2 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 3 | 2 | sbimi 2074 | . . 3 ⊢ ([𝑦 / 𝑥]𝑥 = 𝑦 → [𝑦 / 𝑥](𝜑 ↔ 𝜓)) |
| 4 | 1, 3 | ax-mp 5 | . 2 ⊢ [𝑦 / 𝑥](𝜑 ↔ 𝜓) |
| 5 | sbie.1 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
| 6 | 5 | sbf 2271 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) |
| 7 | 6 | sblbis 2309 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)) |
| 8 | 4, 7 | mpbi 230 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-12 2177 ax-13 2376 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-sb 2065 |
| This theorem is referenced by: sbied 2507 2sbiev 2509 cbvmo 2603 cbveu 2606 cbvab 2813 clelsb2OLD 2869 cbvralf 3359 cbvreu 3427 cbvrab 3478 nfcdeq 3782 cbvralcsf 3940 cbvreucsf 3942 cbvrabcsf 3943 cbvopab1g 5216 cbvmptfg 5250 cbviota 6521 cbvriota 7399 nd1 10623 nd2 10624 sbcrexgOLD 42774 |
| Copyright terms: Public domain | W3C validator |