![]() |
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 2497 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2475 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2069. (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 2069 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
2 | equequ2 2030 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
3 | 2 | imbi1d 342 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) |
4 | 3 | albidv 1924 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) |
5 | 4 | equsalvw 2008 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
6 | 1, 5 | bitri 275 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 [wsb 2068 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 |
This theorem is referenced by: 2sb6 2090 sb1v 2091 sbrimvw 2095 sbievw 2096 sbcom3vv 2099 nfs1v 2154 sb4av 2237 sb6a 2250 sb5 2268 sb56OLD 2270 sbiev 2309 sb8v 2349 sb8f 2350 2eu6 2653 nfabdw 2927 nfabdwOLD 2928 elab6g 3658 ab0OLD 4374 disj 4446 iota4 6521 bj-ax12ssb 35473 bj-sbievwd 35598 bj-hbs1 35628 bj-hbsb2av 35630 bj-sbievw1 35662 bj-sbievw2 35663 bj-sbievw 35664 wl-lem-moexsb 36371 absnsb 45672 ichnfimlem 46066 |
Copyright terms: Public domain | W3C validator |