# Metamath Proof Explorer

## 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}=\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)$
Assertion msubty ${⊢}\left({F}:{A}⟶{R}\wedge {A}\subseteq {V}\wedge {X}\in {E}\right)\to {1}^{st}\left({S}\left({F}\right)\left({X}\right)\right)={1}^{st}\left({X}\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 eqid ${⊢}\mathrm{mRSubst}\left({T}\right)=\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),\mathrm{mRSubst}\left({T}\right)\left({F}\right)\left({2}^{nd}\left({X}\right)\right)⟩$
7 fvex ${⊢}{1}^{st}\left({X}\right)\in \mathrm{V}$
8 fvex ${⊢}\mathrm{mRSubst}\left({T}\right)\left({F}\right)\left({2}^{nd}\left({X}\right)\right)\in \mathrm{V}$
9 7 8 op1std ${⊢}{S}\left({F}\right)\left({X}\right)=⟨{1}^{st}\left({X}\right),\mathrm{mRSubst}\left({T}\right)\left({F}\right)\left({2}^{nd}\left({X}\right)\right)⟩\to {1}^{st}\left({S}\left({F}\right)\left({X}\right)\right)={1}^{st}\left({X}\right)$
10 6 9 syl ${⊢}\left({F}:{A}⟶{R}\wedge {A}\subseteq {V}\wedge {X}\in {E}\right)\to {1}^{st}\left({S}\left({F}\right)\left({X}\right)\right)={1}^{st}\left({X}\right)$