![]() |
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 2504 and sbiev 2312 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 2089 | . 2 ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) |
3 | sbv 2085 | . 2 ⊢ ([𝑦 / 𝑥]𝜓 ↔ 𝜓) | |
4 | 2, 3 | bitri 275 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 [wsb 2061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-sb 2062 |
This theorem is referenced by: sbiedvw 2092 2sbievw 2093 sbievw2 2095 cbvsbv 2097 sbco4 2099 sbid2vw 2256 2mosOLD 2647 eqabbw 2812 sbralieALT 3356 rabrabi 3452 elabgw 3678 ralab 3699 sbcco2 3817 sbcie2g 3833 csbied 3945 dfss2 3980 unabw 4312 notabw 4318 ab0w 4384 ab0orv 4388 2reu8i 47062 ichcircshi 47378 |
Copyright terms: Public domain | W3C validator |