| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sbievw | Structured version Visualization version GIF version | ||
| Description: Conversion of implicit substitution to explicit substitution. Version of sbie 2507 and sbiev 2314 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Aug-2025.) |
| Ref | Expression |
|---|---|
| sbievw.is | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| sbievw | ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbievw.is | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | sbbiiev 2092 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
| 3 | sbv 2088 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 [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 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 |
| This theorem is referenced by: sbiedvw 2095 2sbievw 2096 sbievw2 2098 cbvsbv 2100 sbco4 2102 sbid2vw 2259 2mosOLD 2650 eqabbw 2815 sbralieALT 3359 rabrabi 3456 elabgw 3677 ralab 3697 sbcco2 3815 sbcie2g 3829 csbied 3935 dfss2 3969 unabw 4307 notabw 4313 ab0w 4379 ab0orv 4383 2reu8i 47125 ichcircshi 47441 |
| Copyright terms: Public domain | W3C validator |