Metamath Proof Explorer


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 V X E 2 nd S F X = O F 2 nd 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 V X E S F X = 1 st X O F 2 nd X
7 fvex 1 st X V
8 fvex O F 2 nd X V
9 7 8 op2ndd S F X = 1 st X O F 2 nd X 2 nd S F X = O F 2 nd X
10 6 9 syl F : A R A V X E 2 nd S F X = O F 2 nd X