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 2509). Theorem sb6f 2527 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2505 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  2280  sb6a  2293  sb5  2310  sb8v  2383  sb8f  2384  2eu6  2682  nfabdw  2944  elab6g  3623  iota4  6519  axregs  35807  in-ax8  37013  mh-setind  37324  regsfromregtco  37326  regsfromsetind  37327  regsfromunir1  37328  bj-df-sb  37549  bj-dfsbc  37551  bj-ax12ssb  37557  bj-sbievwd  37679  bj-hbs1  37724  bj-hbsb2av  37726  bj-sbievw1  37757  bj-sbievw2  37758  bj-sbievw  37759  wl-sbid2ft  38477  wl-sb9v  38481  wl-lem-moexsb  38500  absnsb  48096  ichnfimlem  48544