Theorem sb6 2089

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 2500). Theorem sb6f 2533 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2495 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 2157. (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 2029	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 344	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1917	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2006	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 277	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531  [wsb 2065

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 1907  ax-6 1966  ax-7 2011

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066

This theorem is referenced by:  2sb6  2090  sb1v  2091  sb4vOLD  2092  sb2vOLD  2093  sbrimvlem  2097  sbievw  2099  sbcom3vv  2102  nfs1v  2156  sb4av  2240  sb6a  2255  sb56  2273  sb5OLD  2277  sbnvOLD  2318  sbiev  2326  sbequivvOLD  2330  nfsbvOLD  2346  2eu6  2740  nfabdw  3000  iota4  6330  bj-ax12ssb  33986  bj-hbs1  34129  bj-hbsb2av  34131  bj-sbievw1  34164  bj-sbievw2  34165  bj-sbievw  34166  wl-lem-moexsb  34798  wl-dfralsb  34831  wl-dfrabsb  34855  absnsb  43256