Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sb6 | Structured version Visualization version GIF version |
Description: Alternate definition of substitution when variables are disjoint. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" also holds without a disjoint variable condition (sb2 2479). Theorem sb6f 2500 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2474 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2073. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2160. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.) |
Ref | Expression |
---|---|
sb6 | ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sb 2073 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | equequ2 2036 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
3 | 2 | imbi1d 345 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albidv 1928 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | 4 | equsalvw 2013 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
6 | 1, 5 | bitri 278 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 [wsb 2072 |
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 ax-7 2018 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-sb 2073 |
This theorem is referenced by: 2sb6 2094 sb1v 2095 sbrimvlem 2099 sbievw 2101 sbcom3vv 2104 nfs1v 2159 sb4av 2243 sb6a 2257 sb5 2274 sb56OLD 2276 sbiev 2315 2eu6 2657 nfabdw 2920 nfabdwOLD 2921 elab6g 3568 ab0OLD 4276 disj 4348 iota4 6339 bj-ax12ssb 34525 bj-sbievwd 34650 bj-hbs1 34680 bj-hbsb2av 34682 bj-sbievw1 34715 bj-sbievw2 34716 bj-sbievw 34717 wl-lem-moexsb 35409 absnsb 44136 ichnfimlem 44531 |
Copyright terms: Public domain | W3C validator |