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 2267 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2094 can be proved directly by chaining equsv 2011 with sb6 2091. (Contributed by BJ, 22-Dec-2020.) |
Ref | Expression |
---|---|
sbv | ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spsbe 2088 | . . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑) | |
2 | ax5e 1920 | . . 3 ⊢ (∃𝑥𝜑 → 𝜑) | |
3 | 1, 2 | syl 17 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑) |
4 | ax-5 1918 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) | |
5 | stdpc4 2074 | . . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑) | |
6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑) |
7 | 3, 6 | impbii 212 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∀wal 1541 ∃wex 1787 [wsb 2070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 |
This theorem depends on definitions: df-bi 210 df-ex 1788 df-sb 2071 |
This theorem is referenced by: sbcom4 2095 sbievw2 2103 sbcg 3771 vn0 4250 eq0 4255 ab0w 4285 ab0OLD 4287 ab0orv 4290 eq0rdv 4316 rzal 4417 ralf0 4422 iuninc 30616 measiuns 31894 ballotlemodife 32173 xpab 33389 mptsnunlem 35243 ichv 44572 ichf 44573 |
Copyright terms: Public domain | W3C validator |