Theorem msubval

Description: A substitution applied to an expression. (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 )
	msubffval.o	|- O = ( mRSubst ` T )
Assertion	msubval	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` 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		msubffval.o	|- O = ( mRSubst ` T )
6	1 2 3 4 5	msubfval	|- ( ( F : A --> R /\ A C_ V ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
7	6	3adant3	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( S ` F ) = ( e e. E |-> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. ) )
8		simpr	|- ( ( ( F : A --> R /\ A C_ V /\ X e. E ) /\ e = X ) -> e = X )
9	8	fveq2d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. E ) /\ e = X ) -> ( 1st ` e ) = ( 1st ` X ) )
10	8	fveq2d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. E ) /\ e = X ) -> ( 2nd ` e ) = ( 2nd ` X ) )
11	10	fveq2d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. E ) /\ e = X ) -> ( ( O ` F ) ` ( 2nd ` e ) ) = ( ( O ` F ) ` ( 2nd ` X ) ) )
12	9 11	opeq12d	|- ( ( ( F : A --> R /\ A C_ V /\ X e. E ) /\ e = X ) -> <. ( 1st ` e ) , ( ( O ` F ) ` ( 2nd ` e ) ) >. = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. )
13		simp3	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> X e. E )
14		opex	|- <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. e. _V
15	14	a1i	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. e. _V )
16	7 12 13 15	fvmptd	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. )