![]() |
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 2472). Theorem sb6f 2490 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2468 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2060. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2146. (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 2060 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | equequ2 2021 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
3 | 2 | imbi1d 340 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albidv 1915 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | 4 | equsalvw 1999 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
6 | 1, 5 | bitri 274 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 [wsb 2059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 |
This theorem is referenced by: 2sb6 2081 sb1v 2082 sbrimvw 2086 sbievw 2087 sbcom3vv 2090 nfs1v 2145 sb4av 2231 sb6a 2244 sb5 2262 sb56OLD 2264 sbiev 2303 sb8v 2342 sb8f 2343 2eu6 2645 nfabdw 2915 nfabdwOLD 2916 elab6g 3655 ab0OLD 4379 disj 4451 iota4 6534 bj-ax12ssb 36322 bj-sbievwd 36447 bj-hbs1 36477 bj-hbsb2av 36479 bj-sbievw1 36510 bj-sbievw2 36511 bj-sbievw 36512 wl-sbid2ft 37200 wl-sb9v 37204 wl-lem-moexsb 37223 absnsb 46591 ichnfimlem 46984 |
Copyright terms: Public domain | W3C validator |