Metamath Proof Explorer


Definition df-mvsb

Description: Define substitution applied to a valuation. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mvsb mVSubst=tVsmx|sranmSubsttmmVLtvmVRtmdommEvaltsmVHtvx=vmVRtmmEvaltsmVHtv

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvsb classmVSubst
1 vt setvart
2 cvv classV
3 vs setvars
4 vm setvarm
5 vx setvarx
6 3 cv setvars
7 cmsub classmSubst
8 1 cv setvart
9 8 7 cfv classmSubstt
10 9 crn classranmSubstt
11 6 10 wcel wffsranmSubstt
12 4 cv setvarm
13 cmvl classmVL
14 8 13 cfv classmVLt
15 12 14 wcel wffmmVLt
16 11 15 wa wffsranmSubsttmmVLt
17 vv setvarv
18 cmvar classmVR
19 8 18 cfv classmVRt
20 cmevl classmEval
21 8 20 cfv classmEvalt
22 21 cdm classdommEvalt
23 cmvh classmVH
24 8 23 cfv classmVHt
25 17 cv setvarv
26 25 24 cfv classmVHtv
27 26 6 cfv classsmVHtv
28 12 27 22 wbr wffmdommEvaltsmVHtv
29 28 17 19 wral wffvmVRtmdommEvaltsmVHtv
30 5 cv setvarx
31 12 27 21 co classmmEvaltsmVHtv
32 17 19 31 cmpt classvmVRtmmEvaltsmVHtv
33 30 32 wceq wffx=vmVRtmmEvaltsmVHtv
34 16 29 33 w3a wffsranmSubsttmmVLtvmVRtmdommEvaltsmVHtvx=vmVRtmmEvaltsmVHtv
35 34 3 4 5 coprab classsmx|sranmSubsttmmVLtvmVRtmdommEvaltsmVHtvx=vmVRtmmEvaltsmVHtv
36 1 2 35 cmpt classtVsmx|sranmSubsttmmVLtvmVRtmdommEvaltsmVHtvx=vmVRtmmEvaltsmVHtv
37 0 36 wceq wffmVSubst=tVsmx|sranmSubsttmmVLtvmVRtmdommEvaltsmVHtvx=vmVRtmmEvaltsmVHtv