| 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 2270 for a version without disjoint variable condition on 𝑥, 𝜑. If one adds a disjoint variable condition on 𝑥, 𝑡, then sbv 2087 can be proved directly by chaining equsv 2001 with sb6 2084. (Contributed by BJ, 22-Dec-2020.) | 
| Ref | Expression | 
|---|---|
| sbv | ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | spsbe 2081 | . . 3 ⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑) | |
| 2 | ax5e 1911 | . . 3 ⊢ (∃𝑥𝜑 → 𝜑) | |
| 3 | 1, 2 | syl 17 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 → 𝜑) | 
| 4 | ax-5 1909 | . . 3 ⊢ (𝜑 → ∀𝑥𝜑) | |
| 5 | stdpc4 2067 | . . 3 ⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑) | |
| 6 | 4, 5 | syl 17 | . 2 ⊢ (𝜑 → [𝑡 / 𝑥]𝜑) | 
| 7 | 3, 6 | impbii 209 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∀wal 1537 ∃wex 1778 [wsb 2063 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-sb 2064 | 
| This theorem is referenced by: sbcom4 2088 sbievw 2092 sbievw2 2097 sbabel 2937 sbcg 3862 vn0 4344 eq0 4349 ab0w 4378 ab0orv 4382 eq0rdv 4406 rzal 4508 ralf0 4513 iuninc 32574 measiuns 34219 ballotlemodife 34501 xpab 35727 subsym1 36429 mptsnunlem 37340 ichv 47441 ichf 47442 | 
| Copyright terms: Public domain | W3C validator |