Metamath Proof Explorer


Theorem mvhval

Description: Value of the function mapping variables to their corresponding variable expressions. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvhfval.v V = mVR T
mvhfval.y Y = mType T
mvhfval.h H = mVH T
Assertion mvhval X V H X = Y X ⟨“ X ”⟩

Proof

Step Hyp Ref Expression
1 mvhfval.v V = mVR T
2 mvhfval.y Y = mType T
3 mvhfval.h H = mVH T
4 fveq2 v = X Y v = Y X
5 s1eq v = X ⟨“ v ”⟩ = ⟨“ X ”⟩
6 4 5 opeq12d v = X Y v ⟨“ v ”⟩ = Y X ⟨“ X ”⟩
7 1 2 3 mvhfval H = v V Y v ⟨“ v ”⟩
8 opex Y X ⟨“ X ”⟩ V
9 6 7 8 fvmpt X V H X = Y X ⟨“ X ”⟩