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 2513). Theorem sb6f 2531 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2509 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 2195. (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  sbievwOLD  2132  nfs1v  2194  sb4av  2282  sb6a  2296  sb5  2313  sbievOLD  2350  sb8v  2387  sb8f  2388  2eu6  2686  nfabdw  2948  elab6g  3630  iota4  6521  axregs  35611  in-ax8  36795  mh-setind  37106  regsfromregtco  37108  regsfromsetind  37109  regsfromunir1  37110  bj-df-sb  37331  bj-dfsbc  37333  bj-ax12ssb  37339  bj-sbievwd  37461  bj-hbs1  37506  bj-hbsb2av  37508  bj-sbievw1  37539  bj-sbievw2  37540  bj-sbievw  37541  wl-sbid2ft  38259  wl-sb9v  38263  wl-lem-moexsb  38282  absnsb  47824  ichnfimlem  48272