![]() |
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 2482). Theorem sb6f 2500 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2478 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2063. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2155. (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 2063 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | equequ2 2023 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
3 | 2 | imbi1d 341 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albidv 1918 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | 4 | equsalvw 2001 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
6 | 1, 5 | bitri 275 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 [wsb 2062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 |
This theorem is referenced by: 2sb6 2084 sb1v 2085 sbrimvw 2089 sbbiiev 2090 sbievwOLD 2092 nfs1v 2154 sb4av 2242 sb6a 2256 sb5 2274 sbievOLD 2314 sb8v 2353 sb8f 2354 2eu6 2655 nfabdw 2925 elab6g 3669 disj 4456 iota4 6544 in-ax8 36207 bj-ax12ssb 36641 bj-sbievwd 36765 bj-hbs1 36795 bj-hbsb2av 36797 bj-sbievw1 36828 bj-sbievw2 36829 bj-sbievw 36830 wl-sbid2ft 37526 wl-sb9v 37530 wl-lem-moexsb 37549 absnsb 46977 ichnfimlem 47388 |
Copyright terms: Public domain | W3C validator |