Theorem msubrsub

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	msubrsub	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 2nd ` ( ( S ` F ) ` 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	msubval	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. )
7		fvex	|- ( 1st ` X ) e. _V
8		fvex	|- ( ( O ` F ) ` ( 2nd ` X ) ) e. _V
9	7 8	op2ndd	|- ( ( ( S ` F ) ` X ) = <. ( 1st ` X ) , ( ( O ` F ) ` ( 2nd ` X ) ) >. -> ( 2nd ` ( ( S ` F ) ` X ) ) = ( ( O ` F ) ` ( 2nd ` X ) ) )
10	6 9	syl	|- ( ( F : A --> R /\ A C_ V /\ X e. E ) -> ( 2nd ` ( ( S ` F ) ` X ) ) = ( ( O ` F ) ` ( 2nd ` X ) ) )