Theorem mexval2

Description: The set of expressions, which are pairs whose first element is a typecode, and whose second element is a list of constants and variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mexval.k	|- K = ( mTC ` T )
	mexval.e	|- E = ( mEx ` T )
	mexval2.c	|- C = ( mCN ` T )
	mexval2.v	|- V = ( mVR ` T )
Assertion	mexval2	|- E = ( K X. Word ( C u. V ) )

Proof

Step	Hyp	Ref	Expression
1		mexval.k	|- K = ( mTC ` T )
2		mexval.e	|- E = ( mEx ` T )
3		mexval2.c	|- C = ( mCN ` T )
4		mexval2.v	|- V = ( mVR ` T )
5		eqid	|- ( mREx ` T ) = ( mREx ` T )
6	1 2 5	mexval	|- E = ( K X. ( mREx ` T ) )
7	3 4 5	mrexval	|- ( T e. _V -> ( mREx ` T ) = Word ( C u. V ) )
8	7	xpeq2d	|- ( T e. _V -> ( K X. ( mREx ` T ) ) = ( K X. Word ( C u. V ) ) )
9	6 8	syl5eq	|- ( T e. _V -> E = ( K X. Word ( C u. V ) ) )
10		0xp	|- ( (/) X. Word ( C u. V ) ) = (/)
11	10	eqcomi	|- (/) = ( (/) X. Word ( C u. V ) )
12		fvprc	|- ( -. T e. _V -> ( mEx ` T ) = (/) )
13	2 12	syl5eq	|- ( -. T e. _V -> E = (/) )
14		fvprc	|- ( -. T e. _V -> ( mTC ` T ) = (/) )
15	1 14	syl5eq	|- ( -. T e. _V -> K = (/) )
16	15	xpeq1d	|- ( -. T e. _V -> ( K X. Word ( C u. V ) ) = ( (/) X. Word ( C u. V ) ) )
17	11 13 16	3eqtr4a	|- ( -. T e. _V -> E = ( K X. Word ( C u. V ) ) )
18	9 17	pm2.61i	|- E = ( K X. Word ( C u. V ) )