Step |
Hyp |
Ref |
Expression |
1 |
|
msubffval.v |
⊢ 𝑉 = ( mVR ‘ 𝑇 ) |
2 |
|
msubffval.r |
⊢ 𝑅 = ( mREx ‘ 𝑇 ) |
3 |
|
msubffval.s |
⊢ 𝑆 = ( mSubst ‘ 𝑇 ) |
4 |
|
msubffval.e |
⊢ 𝐸 = ( mEx ‘ 𝑇 ) |
5 |
|
eqid |
⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 ) |
6 |
1 2 3 4 5
|
msubval |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = 〈 ( 1st ‘ 𝑋 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) 〉 ) |
7 |
|
fvex |
⊢ ( 1st ‘ 𝑋 ) ∈ V |
8 |
|
fvex |
⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) ∈ V |
9 |
7 8
|
op1std |
⊢ ( ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) = 〈 ( 1st ‘ 𝑋 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝐹 ) ‘ ( 2nd ‘ 𝑋 ) ) 〉 → ( 1st ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) ) |
10 |
6 9
|
syl |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ 𝐸 ) → ( 1st ‘ ( ( 𝑆 ‘ 𝐹 ) ‘ 𝑋 ) ) = ( 1st ‘ 𝑋 ) ) |