|   | 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 2483). Theorem sb6f 2501 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2479 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2064. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2156. (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 2064 | . 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | |
| 2 | equequ2 2024 | . . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡)) | |
| 3 | 2 | imbi1d 341 | . . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑))) | 
| 4 | 3 | albidv 1919 | . . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))) | 
| 5 | 4 | equsalvw 2002 | . 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | 
| 6 | 1, 5 | bitri 275 | 1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1537 [wsb 2063 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 | 
| This theorem is referenced by: 2sb6 2085 sb1v 2086 sbrimvw 2090 sbbiiev 2091 sbievwOLD 2093 nfs1v 2155 sb4av 2243 sb6a 2257 sb5 2275 sbievOLD 2314 sb8v 2354 sb8f 2355 2eu6 2656 nfabdw 2926 elab6g 3668 disj 4449 iota4 6541 in-ax8 36226 bj-ax12ssb 36660 bj-sbievwd 36784 bj-hbs1 36814 bj-hbsb2av 36816 bj-sbievw1 36847 bj-sbievw2 36848 bj-sbievw 36849 wl-sbid2ft 37547 wl-sb9v 37551 wl-lem-moexsb 37570 absnsb 47044 ichnfimlem 47455 | 
| Copyright terms: Public domain | W3C validator |