Definition df-msub 30177

Description: Define a substitution of expressions given a mapping from variables to expressions. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-msub	|- mSubst = ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mEx ` t ) |-> <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )

Distinct variable group:   e, f, t

Detailed syntax breakdown of Definition df-msub

Step	Hyp	Ref	Expression
1		cmsub 30157	. 2 class mSubst
2		vt	. . 3 setvar t
3		cvv 3056	. . 3 class _V
4		vf	. . . 4 setvar f
5	2	cv 1453	. . . . . 6 class t
6		cmrex 30152	. . . . . 6 class mREx
7	5, 6	cfv 5600	. . . . 5 class (mREx ` t )
8		cmvar 30147	. . . . . 6 class mVR
9	5, 8	cfv 5600	. . . . 5 class (mVR ` t )
10		cpm 7498	. . . . 5 class ^pm
11	7, 9, 10	co 6314	. . . 4 class ( (mREx ` t ) ^pm (mVR ` t ) )
12		ve	. . . . 5 setvar e
13		cmex 30153	. . . . . 6 class mEx
14	5, 13	cfv 5600	. . . . 5 class (mEx ` t )
15	12	cv 1453	. . . . . . 7 class e
16		c1st 6817	. . . . . . 7 class 1st
17	15, 16	cfv 5600	. . . . . 6 class ( 1st ` e )
18		c2nd 6818	. . . . . . . 8 class 2nd
19	15, 18	cfv 5600	. . . . . . 7 class ( 2nd ` e )
20	4	cv 1453	. . . . . . . 8 class f
21		cmrsub 30156	. . . . . . . . 9 class mRSubst
22	5, 21	cfv 5600	. . . . . . . 8 class (mRSubst ` t )
23	20, 22	cfv 5600	. . . . . . 7 class ( (mRSubst ` t ) ` f )
24	19, 23	cfv 5600	. . . . . 6 class ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) )
25	17, 24	cop 3985	. . . . 5 class <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >.
26	12, 14, 25	cmpt 4474	. . . 4 class ( e e. (mEx ` t ) |-> <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. )
27	4, 11, 26	cmpt 4474	. . 3 class ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mEx ` t ) |-> <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) )
28	2, 3, 27	cmpt 4474	. 2 class ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mEx ` t ) |-> <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )
29	1, 28	wceq 1454	1 wff mSubst = ( t e. _V |-> ( f e. ( (mREx ` t ) ^pm (mVR ` t ) ) |-> ( e e. (mEx ` t ) |-> <. ( 1st ` e ) , ( ( (mRSubst ` t ) ` f ) ` ( 2nd ` e ) ) >. ) ) )

This definition is referenced by:  msubffval  30209