Description: Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | df-mvsb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmvsb | |
|
1 | vt | |
|
2 | cvv | |
|
3 | vs | |
|
4 | vm | |
|
5 | vx | |
|
6 | 3 | cv | |
7 | cmsub | |
|
8 | 1 | cv | |
9 | 8 7 | cfv | |
10 | 9 | crn | |
11 | 6 10 | wcel | |
12 | 4 | cv | |
13 | cmvl | |
|
14 | 8 13 | cfv | |
15 | 12 14 | wcel | |
16 | 11 15 | wa | |
17 | vv | |
|
18 | cmvar | |
|
19 | 8 18 | cfv | |
20 | cmevl | |
|
21 | 8 20 | cfv | |
22 | 21 | cdm | |
23 | cmvh | |
|
24 | 8 23 | cfv | |
25 | 17 | cv | |
26 | 25 24 | cfv | |
27 | 26 6 | cfv | |
28 | 12 27 22 | wbr | |
29 | 28 17 19 | wral | |
30 | 5 | cv | |
31 | 12 27 21 | co | |
32 | 17 19 31 | cmpt | |
33 | 30 32 | wceq | |
34 | 16 29 33 | w3a | |
35 | 34 3 4 5 | coprab | |
36 | 1 2 35 | cmpt | |
37 | 0 36 | wceq | |