Definition df-sb 2093

Description: Define proper substitution. We write [𝑡 / 𝑥]𝜑 for "the wff obtained by properly substituting 𝑡 for 𝑥 in the wff 𝜑". Thus, 𝑡 properly replaces 𝑥. For example, [𝑡 / 𝑥]𝑧 ∈ 𝑥 is 𝑧 ∈ 𝑡 (when 𝑥 and 𝑧 are distinct), as shown in elsb2 2161.

In practice, the definiens reduces to "∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) " (see just3-df 2090). Here it is followed by the same expression with a fresh dummy variable 𝑧, making explicit the independence of the dummy variable's name (see just2-df 2089). This is a necessity of Metamath supporting axiom dependency lists. See justify-df 2087 for more information about this technique.

The added conjunct will make some proofs appear duplicated. Alternately, one may first prove as a lemma the same theorem under a disjoint variable condition on the substituted and the substituting variables, then obtain the original theorem by applying that lemma twice.

Our notation, without the alpha-renamed repetition, was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "𝜑(𝑡) is the wff obtained by properly substituting 𝑡 for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑡, then 𝜑(𝑡) is 𝑡 = 𝑡, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation avoids this problem.

A closely related notation, (𝑦 ∣ 𝑥)𝜑, was introduced in Bourbaki's Set Theory (Chapter 1, Description of Formal Mathematic, 1953).

Most textbooks define proper substitution recursively by considering various cases involving free and bound variables. Instead, we use a single formula that is exactly equivalent and serves as a direct definition. We later prove that this definition has the expected properties of proper substitution; see sbequ 2118, sbcom2 2208, and sbid2v 2542.

This definition remains valid when 𝑥 and 𝑡 are replaced with the same variable, as shown by sbid 2292. This is achieved by applying Tarski's definition sb6 2120 twice, which is valid for disjoint variables, and introducing a dummy variable 𝑦 that isolates 𝑥 from 𝑡, as in dfsb7 2315 relative to sb5 2312. We can also achieve this by having 𝑥 free in the first conjunct and bound in the second, as the alternate definition dfsb1 2514 shows. Another version that mixes free and bound variables is dfsb3 2527. When 𝑥 and 𝑡 are distinct, proper substitution can be expressed more simply using sb5 2312 and sb6 2120.

Note that each variable in the definiens is either entirely bound (𝑥, 𝑦) or entirely free (𝑡). The definiens also uses only primitive symbols.

Prefer the more general form dfsb 2095 when axiom usage is unimportant. It provides a simpler right hand side together with a proof of its alpha-renaming. (Contributed by NM, 10-May-1993.) Revised from the original definition dfsb1 2514. (Revised by BJ, 22-Dec-2020.) Support alpha-renaming. (Revised by Wolf Lammen, 4-Jun-2026.)

Assertion

Ref	Expression
df-sb	⊢ ([𝑡 / 𝑥]𝜑 ↔ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))))

Distinct variable groups:   𝑥,𝑦,𝑧   𝑦,𝑡,𝑧   𝜑,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑡)

Detailed syntax breakdown of Definition df-sb

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vt	. . 3 setvar 𝑡
4	1, 2, 3	wsb 2092	. 2 wff [𝑡 / 𝑥]𝜑
5		vy	. . . . . 6 setvar 𝑦
6	5, 3	weq 1984	. . . . 5 wff 𝑦 = 𝑡
7	2, 5	weq 1984	. . . . . . 7 wff 𝑥 = 𝑦
8	7, 1	wi 4	. . . . . 6 wff (𝑥 = 𝑦 → 𝜑)
9	8, 2	wal 1560	. . . . 5 wff ∀𝑥(𝑥 = 𝑦 → 𝜑)
10	6, 9	wi 4	. . . 4 wff (𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
11	10, 5	wal 1560	. . 3 wff ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
12		vz	. . . . . 6 setvar 𝑧
13	12, 3	weq 1984	. . . . 5 wff 𝑧 = 𝑡
14	2, 12	weq 1984	. . . . . . 7 wff 𝑥 = 𝑧
15	14, 1	wi 4	. . . . . 6 wff (𝑥 = 𝑧 → 𝜑)
16	15, 2	wal 1560	. . . . 5 wff ∀𝑥(𝑥 = 𝑧 → 𝜑)
17	13, 16	wi 4	. . . 4 wff (𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))
18	17, 12	wal 1560	. . 3 wff ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))
19	11, 18	wa 399	. 2 wff (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
20	4, 19	wb 208	1 wff ([𝑡 / 𝑥]𝜑 ↔ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) ∧ ∀𝑧(𝑧 = 𝑡 → ∀𝑥(𝑥 = 𝑧 → 𝜑))))

This definition is referenced by:  dfsbimp  2094  dfsb  2095  sbt  2097  stdpc4  2100  sbi1  2105