Nearby theorems
|
|
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > wssb | Structured version Visualization version GIF version | ||
| Description: Syntax for the substitution of a variable for a variable in a formula. (Contributed by BJ, 22-Dec-2020.) |
| Ref | Expression |
|---|---|
| wph | wff 𝜑 |
| vx | setvar 𝑥 |
| vt | setvar 𝑡 |
| Ref | Expression |
|---|---|
| wssb | wff [𝑡/𝑥]b𝜑 |
| Colors of variables: wff setvar class |
| Copyright terms: Public domain | W3C validator |