Theorem sb6 2064

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 2456). Theorem sb6f 2489 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2455 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2041. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2124. (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 2041	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2008	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 343	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1896	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 1985	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 276	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1518  [wsb 2040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-sb 2041

This theorem is referenced by:  sb4vOLD  2065  sb2vOLD  2066  sbievw  2070  sbcom3vv  2071  sb6a  2220  nfs1v  2235  sb56  2239  sb5OLD  2242  2sb6  2244  sbnvOLD  2285  sbiev  2293  sbequivvOLD  2295  nfsbvOLD  2311  2sb8evOLD  2330  2eu6  2712  iota4  6199  bj-ax12ssb  33534  bj-hbs1  33628  bj-hbsb2av  33630  bj-sbievw1  33683  bj-sbievw2  33684  bj-sbievw  33685  wl-lem-moexsb  34281  wl-dfralsb  34314  wl-dfrabsb  34338  absnsb  42732