Theorem sb6 2091

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 2484). Theorem sb6f 2502 replaces the disjoint variable condition with a nonfreeness hypothesis. Theorem sb4b 2480 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) Revise df-sb 2069. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2163. (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 2070	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2028	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 341	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1922	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2006	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 275	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  2sb6  2092  sb1v  2093  sbrimvw  2097  sbbiiev  2098  sbievwOLD  2100  nfs1v  2162  sb4av  2252  sb6a  2266  sb5  2283  sbievOLD  2321  sb8v  2358  sb8f  2359  2eu6  2658  nfabdw  2921  elab6g  3612  iota4  6474  axregs  35302  in-ax8  36425  mh-setind  36737  regsfromregtco  36739  regsfromsetind  36740  regsfromunir1  36741  bj-df-sb  36963  bj-dfsbc  36965  bj-ax12ssb  36971  bj-sbievwd  37093  bj-hbs1  37138  bj-hbsb2av  37140  bj-sbievw1  37171  bj-sbievw2  37172  bj-sbievw  37173  wl-sbid2ft  37887  wl-sb9v  37891  wl-lem-moexsb  37910  absnsb  47490  ichnfimlem  47938