Theorem sb6 2118

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 2091. (Revised by BJ, 22-Dec-2020.) Remove use of ax-11 2191. (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 2093	. 2 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
2		equequ2 2046	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑡))
3	2	imbi1d 343	. . . 4 ⊢ (𝑦 = 𝑡 → ((𝑥 = 𝑦 → 𝜑) ↔ (𝑥 = 𝑡 → 𝜑)))
4	3	albidv 1940	. . 3 ⊢ (𝑦 = 𝑡 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
5	4	equsalvw 2024	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
6	1, 5	bitri 277	1 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558  [wsb 2090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091

This theorem is referenced by:  2sb6  2119  sb1v  2120  sbrimvwOLD  2125  sbbiiev  2126  sbievwOLD  2128  nfs1v  2190  sb4av  2279  sb6a  2293  sb5  2310  sbievOLD  2347  sb8v  2384  sb8f  2385  2eu6  2683  nfabdw  2945  elab6g  3628  iota4  6502  axregs  35435  in-ax8  36584  mh-setind  36896  regsfromregtco  36898  regsfromsetind  36899  regsfromunir1  36900  bj-df-sb  37122  bj-dfsbc  37124  bj-ax12ssb  37130  bj-sbievwd  37252  bj-hbs1  37297  bj-hbsb2av  37299  bj-sbievw1  37330  bj-sbievw2  37331  bj-sbievw  37332  wl-sbid2ft  38048  wl-sb9v  38052  wl-lem-moexsb  38071  absnsb  47621  ichnfimlem  48069