Mathbox for Mario Carneiro |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-msub | Structured version Visualization version Unicode version |
Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.) |
Ref | Expression |
---|---|
df-msub | mSubst mREx mVR mEx mRSubst |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmsub 31368 | . 2 mSubst | |
2 | vt | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | vf | . . . 4 | |
5 | 2 | cv 1482 | . . . . . 6 |
6 | cmrex 31363 | . . . . . 6 mREx | |
7 | 5, 6 | cfv 5888 | . . . . 5 mREx |
8 | cmvar 31358 | . . . . . 6 mVR | |
9 | 5, 8 | cfv 5888 | . . . . 5 mVR |
10 | cpm 7858 | . . . . 5 | |
11 | 7, 9, 10 | co 6650 | . . . 4 mREx mVR |
12 | ve | . . . . 5 | |
13 | cmex 31364 | . . . . . 6 mEx | |
14 | 5, 13 | cfv 5888 | . . . . 5 mEx |
15 | 12 | cv 1482 | . . . . . . 7 |
16 | c1st 7166 | . . . . . . 7 | |
17 | 15, 16 | cfv 5888 | . . . . . 6 |
18 | c2nd 7167 | . . . . . . . 8 | |
19 | 15, 18 | cfv 5888 | . . . . . . 7 |
20 | 4 | cv 1482 | . . . . . . . 8 |
21 | cmrsub 31367 | . . . . . . . . 9 mRSubst | |
22 | 5, 21 | cfv 5888 | . . . . . . . 8 mRSubst |
23 | 20, 22 | cfv 5888 | . . . . . . 7 mRSubst |
24 | 19, 23 | cfv 5888 | . . . . . 6 mRSubst |
25 | 17, 24 | cop 4183 | . . . . 5 mRSubst |
26 | 12, 14, 25 | cmpt 4729 | . . . 4 mEx mRSubst |
27 | 4, 11, 26 | cmpt 4729 | . . 3 mREx mVR mEx mRSubst |
28 | 2, 3, 27 | cmpt 4729 | . 2 mREx mVR mEx mRSubst |
29 | 1, 28 | wceq 1483 | 1 mSubst mREx mVR mEx mRSubst |
Colors of variables: wff setvar class |
This definition is referenced by: msubffval 31420 |
Copyright terms: Public domain | W3C validator |