Theorem sb6 2121

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 2099. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2193. (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 2100	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2058	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 344	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1952	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2036	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 278	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099

This theorem is used by:  2sb6  2122  sb1v  2123  sbrimvwOLD  2128  sbbiiev  2129  nfs1v  2192  sb4av  2279  sb6a  2292  sb5  2309  sb8v  2382  sb8f  2383  2eu6  2681  nfabdw  2943  elab6g  3622  iota4  6523  axregs  35875  in-ax8  37137  mh-setind  37448  regsfromregtco  37450  regsfromsetind  37451  regsfromunir1  37452  bj-df-sb  37673  bj-dfsbc  37675  bj-ax12ssb  37681  bj-sbievwd  37803  bj-hbs1  37848  bj-hbsb2av  37850  bj-sbievw1  37881  bj-sbievw2  37882  bj-sbievw  37883  wl-sbid2ft  38614  wl-sb9v  38618  wl-lem-moexsb  38637  absnsb  48233  ichnfimlem  48681