Theorem msubty

Description: The type of a substituted expression is the same as the original type. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	|- V = ( mVR ` T )
	msubffval.r	|- R = ( mREx ` T )
	msubffval.s	|- S = ( mSubst ` T )
	msubffval.e	|- E = ( mEx ` T )
Assertion	msubty	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 1st ` ( ( S ` F ) ` X ) ) = ( 1st ` X ) )

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	|- V = ( mVR ` T )
2		msubffval.r	|- R = ( mREx ` T )
3		msubffval.s	|- S = ( mSubst ` T )
4		msubffval.e	|- E = ( mEx ` T )
5		eqid	|- ( mRSubst ` T ) = ( mRSubst ` T )
6	1 2 3 4 5	msubval	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( ( mRSubst ` T ) ` F ) ` ( 2nd ` X ) ) >. )
7		fvex	|- ( 1st ` X ) e. _V
8		fvex	|- ( ( ( mRSubst ` T ) ` F ) ` ( 2nd ` X ) ) e. _V
9	7 8	op1std	|- ( ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( ( mRSubst ` T ) ` F ) ` ( 2nd ` X ) ) >. -> ( 1st ` ( ( S ` F ) ` X ) ) = ( 1st ` X ) )
10	6 9	syl	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 1st ` ( ( S ` F ) ` X ) ) = ( 1st ` X ) )