Description: Define proper substitution. We write [ t / x ] ph for "the wff obtained by properly substituting t for x in the wff ph ". Thus, t properly replaces x . For example, [ t / x ] z e. x is z e. t (when x and z are distinct), as shown in elsb2 .
In practice, the definiens reduces to " A. y ( y = t -> A. x ( x = y -> ph ) ) " (see just3-df ). Here it is followed by the same expression with a fresh dummy variable z , making explicit the independence of the dummy variable's name (see just2-df ). This is a necessity of Metamath supporting axiom dependency lists. See justify-df 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'sFoundations 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, " ph ( t ) is the wff obtained by properly substituting t for x in ph ( x ) ". For example, if the original ph ( x ) is x = t , then ph ( t ) is t = t , from which we obtain that ph ( x ) is x = x . So what exactly does ph ( x ) mean? Curry's notation avoids this problem.
A closely related notation, ( y | x ) ph , 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 , sbcom2 , and sbid2v .
This definition remains valid when x and t are replaced with the same variable, as shown by sbid . This is achieved by applying Tarski's definition sb6 twice, which is valid for disjoint variables, and introducing a dummy variable y that isolates x from t , as in dfsb7 relative to sb5 . We can also achieve this by having x free in the first conjunct and bound in the second, as the alternate definition dfsb1 shows. Another version that mixes free and bound variables is dfsb3 . When x and t are distinct, proper substitution can be expressed more simply using sb5 and sb6 .
Note that each variable in the definiens is either entirely bound ( x , y ) or entirely free ( t ). The definiens also uses only primitive symbols.
Prefer the more general form dfsb 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 . (Revised by BJ, 22-Dec-2020) Support alpha-renaming. (Revised by Wolf Lammen, 4-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-sb | |- ( [ t / x ] ph <-> ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vt | |- t |
|
| 1 | vx | |- x |
|
| 2 | wph | |- ph |
|
| 3 | 2 1 0 | wsb | |- [ t / x ] ph |
| 4 | vy | |- y |
|
| 5 | 4 | cv | |- y |
| 6 | 0 | cv | |- t |
| 7 | 5 6 | wceq | |- y = t |
| 8 | 1 | cv | |- x |
| 9 | 8 5 | wceq | |- x = y |
| 10 | 9 2 | wi | |- ( x = y -> ph ) |
| 11 | 10 1 | wal | |- A. x ( x = y -> ph ) |
| 12 | 7 11 | wi | |- ( y = t -> A. x ( x = y -> ph ) ) |
| 13 | 12 4 | wal | |- A. y ( y = t -> A. x ( x = y -> ph ) ) |
| 14 | vz | |- z |
|
| 15 | 14 | cv | |- z |
| 16 | 15 6 | wceq | |- z = t |
| 17 | 8 15 | wceq | |- x = z |
| 18 | 17 2 | wi | |- ( x = z -> ph ) |
| 19 | 18 1 | wal | |- A. x ( x = z -> ph ) |
| 20 | 16 19 | wi | |- ( z = t -> A. x ( x = z -> ph ) ) |
| 21 | 20 14 | wal | |- A. z ( z = t -> A. x ( x = z -> ph ) ) |
| 22 | 13 21 | wa | |- ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) |
| 23 | 3 22 | wb | |- ( [ t / x ] ph <-> ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) ) |