![]() |
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 2262 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 2938 sbralie 3354 sbcg 3855 vn0 4337 eq0 4342 ab0w 4372 ab0OLD 4374 ab0orv 4377 eq0rdv 4403 rzal 4507 ralf0 4512 iuninc 31779 measiuns 33203 ballotlemodife 33484 xpab 34683 subsym1 35300 mptsnunlem 36207 ichv 46103 ichf 46104 |
Copyright terms: Public domain | W3C validator |