![]() |
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 2456). Theorem sb6f 2489 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2455 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2041. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2124. (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 2041 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | equequ2 2008 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
3 | 2 | imbi1d 343 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albidv 1896 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | 4 | equsalvw 1985 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
6 | 1, 5 | bitri 276 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1518 [wsb 2040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-sb 2041 |
This theorem is referenced by: sb4vOLD 2065 sb2vOLD 2066 sbievw 2070 sbcom3vv 2071 sb6a 2220 nfs1v 2235 sb56 2239 sb5OLD 2242 2sb6 2244 sbnvOLD 2285 sbiev 2293 sbequivvOLD 2295 nfsbvOLD 2311 2sb8evOLD 2330 2eu6 2712 iota4 6199 bj-ax12ssb 33534 bj-hbs1 33628 bj-hbsb2av 33630 bj-sbievw1 33683 bj-sbievw2 33684 bj-sbievw 33685 wl-lem-moexsb 34281 wl-dfralsb 34314 wl-dfrabsb 34338 absnsb 42732 |
Copyright terms: Public domain | W3C validator |