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 2510). Theorem sb6f 2528 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2506 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  2281  sb6a  2294  sb5  2311  sb8v  2384  sb8f  2385  2eu6  2683  nfabdw  2945  elab6g  3626  iota4  6518  axregs  35673  in-ax8  36852  mh-setind  37163  regsfromregtco  37165  regsfromsetind  37166  regsfromunir1  37167  bj-df-sb  37388  bj-dfsbc  37390  bj-ax12ssb  37396  bj-sbievwd  37518  bj-hbs1  37563  bj-hbsb2av  37565  bj-sbievw1  37596  bj-sbievw2  37597  bj-sbievw  37598  wl-sbid2ft  38316  wl-sb9v  38320  wl-lem-moexsb  38339  absnsb  47923  ichnfimlem  48371