Theorem mexval

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

	Ref	Expression
Hypotheses	mexval.k	|- K = ( mTC ` T )
	mexval.e	|- E = ( mEx ` T )
	mexval.r	|- R = ( mREx ` T )
Assertion	mexval	|- E = ( K X. R )

Proof

Step	Hyp	Ref	Expression
1		mexval.k	|- K = ( mTC ` T )
2		mexval.e	|- E = ( mEx ` T )
3		mexval.r	|- R = ( mREx ` T )
4		fveq2	|- ( t = T -> ( mTC ` t ) = ( mTC ` T ) )
5	4 1	eqtr4di	|- ( t = T -> ( mTC ` t ) = K )
6		fveq2	|- ( t = T -> ( mREx ` t ) = ( mREx ` T ) )
7	6 3	eqtr4di	|- ( t = T -> ( mREx ` t ) = R )
8	5 7	xpeq12d	|- ( t = T -> ( ( mTC ` t ) X. ( mREx ` t ) ) = ( K X. R ) )
9		df-mex	|- mEx = ( t e. _V |-> ( ( mTC ` t ) X. ( mREx ` t ) ) )
10		fvex	|- ( mTC ` t ) e. _V
11		fvex	|- ( mREx ` t ) e. _V
12	10 11	xpex	|- ( ( mTC ` t ) X. ( mREx ` t ) ) e. _V
13	8 9 12	fvmpt3i	|- ( T e. _V -> ( mEx ` T ) = ( K X. R ) )
14		xp0	|- ( K X. (/) ) = (/)
15	14	eqcomi	|- (/) = ( K X. (/) )
16		fvprc	|- ( -. T e. _V -> ( mEx ` T ) = (/) )
17		fvprc	|- ( -. T e. _V -> ( mREx ` T ) = (/) )
18	3 17	syl5eq	|- ( -. T e. _V -> R = (/) )
19	18	xpeq2d	|- ( -. T e. _V -> ( K X. R ) = ( K X. (/) ) )
20	15 16 19	3eqtr4a	|- ( -. T e. _V -> ( mEx ` T ) = ( K X. R ) )
21	13 20	pm2.61i	|- ( mEx ` T ) = ( K X. R )
22	2 21	eqtri	|- E = ( K X. R )