Description: Define the set of expressions, which are strings of constants and variables headed by a typecode constant. (Contributed by Mario Carneiro, 14-Jul-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-mex | |- mEx = ( t e. _V |-> ( ( mTC ` t ) X. ( mREx ` t ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cmex | |- mEx |
|
| 1 | vt | |- t |
|
| 2 | cvv | |- _V |
|
| 3 | cmtc | |- mTC |
|
| 4 | 1 | cv | |- t |
| 5 | 4 3 | cfv | |- ( mTC ` t ) |
| 6 | cmrex | |- mREx |
|
| 7 | 4 6 | cfv | |- ( mREx ` t ) |
| 8 | 5 7 | cxp | |- ( ( mTC ` t ) X. ( mREx ` t ) ) |
| 9 | 1 2 8 | cmpt | |- ( t e. _V |-> ( ( mTC ` t ) X. ( mREx ` t ) ) ) |
| 10 | 0 9 | wceq | |- mEx = ( t e. _V |-> ( ( mTC ` t ) X. ( mREx ` t ) ) ) |