Theorem sb6 2122

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 2508). Theorem sb6f 2526 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2504 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2100. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2194. (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		dfsb 2101	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2059	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 344	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1953	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2037	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 278	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100

This theorem is used by:  2sb6  2123  sb1v  2124  sbrimvwOLD  2129  sbbiiev  2130  nfs1v  2193  sb4av  2279  sb6a  2292  sb5  2309  sb8v  2382  sb8f  2383  2eu6  2681  nfabdw  2943  elab6g  3623  iota4  6514  axregs  35666  in-ax8  36845  mh-setind  37156  regsfromregtco  37158  regsfromsetind  37159  regsfromunir1  37160  bj-df-sb  37381  bj-dfsbc  37383  bj-ax12ssb  37389  bj-sbievwd  37511  bj-hbs1  37556  bj-hbsb2av  37558  bj-sbievw1  37589  bj-sbievw2  37590  bj-sbievw  37591  wl-sbid2ft  38309  wl-sb9v  38313  wl-lem-moexsb  38332  absnsb  47916  ichnfimlem  48364