Theorem msubrsub

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubffval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	msubffval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
	msubffval.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
	msubffval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	msubffval.o	$$⊢O=\mathrm{mRSubst}\left(T\right)$$
Assertion	msubrsub	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to 2^{nd}\left(S\left(F\right)\left(X\right)\right)=O\left(F\right)\left(2^{nd}\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		msubffval.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
2		msubffval.r	$$⊢R=\mathrm{mREx}\left(T\right)$$
3		msubffval.s	$$⊢S=\mathrm{mSubst}\left(T\right)$$
4		msubffval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
5		msubffval.o	$$⊢O=\mathrm{mRSubst}\left(T\right)$$
6	1 2 3 4 5	msubval	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to S\left(F\right)\left(X\right)=⟨1^{st}\left(X\right),O\left(F\right)\left(2^{nd}\left(X\right)\right)⟩$$
7		fvex	$$⊢1^{st}\left(X\right)\in \mathrm{V}$$
8		fvex	$$⊢O\left(F\right)\left(2^{nd}\left(X\right)\right)\in \mathrm{V}$$
9	7 8	op2ndd	$$⊢S\left(F\right)\left(X\right)=⟨1^{st}\left(X\right),O\left(F\right)\left(2^{nd}\left(X\right)\right)⟩\to 2^{nd}\left(S\left(F\right)\left(X\right)\right)=O\left(F\right)\left(2^{nd}\left(X\right)\right)$$
10	6 9	syl	$$⊢\left(F:A⟶R\wedge A\subseteq V\wedge X\in E\right)\to 2^{nd}\left(S\left(F\right)\left(X\right)\right)=O\left(F\right)\left(2^{nd}\left(X\right)\right)$$