| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define proper
substitution. Remark 9.1 in [Megill] p. 447
(p. 15 of the
preprint). For our notation, we use
Our notation 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, " In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a single formula that is exactly equivalent and gives us a direct definition. We later prove that our definition has the properties we expect of proper substitution (see theorems sbequ 1875, sbcom2 1990 and sbid2v 1998).
Note that our definition is valid even when
There are no restrictions on any of the variables, including what
variables may occur in wff |
| Ref | Expression |
|---|---|
| df-sb |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | vx |
. . 3
| |
| 3 | vy |
. . . 4
| |
| 4 | 3 | cv 1585 |
. . 3
|
| 5 | 1, 2, 4 | wsbc 1814 |
. 2
|
| 6 | 2 | cv 1585 |
. . . . 5
|
| 7 | 6, 4 | wceq 1586 |
. . . 4
|
| 8 | 7, 1 | wi 3 |
. . 3
|
| 9 | 7, 1 | wa 337 |
. . . 4
|
| 10 | 9, 2 | wex 1615 |
. . 3
|
| 11 | 8, 10 | wa 337 |
. 2
|
| 12 | 5, 11 | wb 219 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: sbimi 1817 drsb1 1819 sb1 1820 sb2 1821 sbequ1 1822 sbequ2 1823 sbn 1877 sb6 1914 subsym1 14951 |