Theorem sb6 2086

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 2484). Theorem sb6f 2502 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2480 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2066. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2158. (Revised by Steven Nguyen, 7-Jul-2023.) (Proof shortened by Wolf Lammen, 16-Jul-2023.)

Assertion

Ref	Expression
sb6	⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Distinct variable group:   𝑥,𝑡

Allowed substitution hints:   𝜑(𝑥,𝑡)

Proof of Theorem sb6

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sb 2066	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2026	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 341	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1920	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2004	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 275	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066

This theorem is referenced by:  2sb6  2087  sb1v  2088  sbrimvw  2092  sbbiiev  2093  sbievwOLD  2095  nfs1v  2157  sb4av  2245  sb6a  2259  sb5  2277  sbievOLD  2316  sb8v  2355  sb8f  2356  2eu6  2657  nfabdw  2921  elab6g  3653  disj  4430  iota4  6517  in-ax8  36247  bj-ax12ssb  36681  bj-sbievwd  36805  bj-hbs1  36835  bj-hbsb2av  36837  bj-sbievw1  36868  bj-sbievw2  36869  bj-sbievw  36870  wl-sbid2ft  37568  wl-sb9v  37572  wl-lem-moexsb  37591  absnsb  47023  ichnfimlem  47444