![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbv | Structured version Visualization version GIF version |
Description: Substitution for a variable not occurring in a proposition. See sbf 2263 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2091 can be proved directly by chaining equsv 2006 with sb6 2088. (Contributed by BJ, 22-Dec-2020.) |
Ref | Expression |
---|---|
sbv | ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbe 2085 | . . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑) | |
2 | ax5e 1915 | . . 3 ⊢ (∃𝑥𝜑 → 𝜑) | |
3 | 1, 2 | syl 17 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑) |
4 | ax-5 1913 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) | |
5 | stdpc4 2071 | . . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑) |
7 | 3, 6 | impbii 208 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wal 1539 ∃wex 1781 [wsb 2067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 |
This theorem depends on definitions: df-bi 206 df-ex 1782 df-sb 2068 |
This theorem is referenced by: sbcom4 2092 sbievw2 2099 sbabel 2939 sbcg 3816 vn0 4296 eq0 4301 ab0w 4331 ab0OLD 4333 ab0orv 4336 eq0rdv 4362 rzal 4464 ralf0 4469 iuninc 31308 measiuns 32628 ballotlemodife 32909 xpab 34109 subsym1 34837 mptsnunlem 35747 ichv 45542 ichf 45543 |
Copyright terms: Public domain | W3C validator |