Metamath Proof Explorer


Theorem mvhf1

Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mvhf.v V = mVR T
mvhf.e E = mEx T
mvhf.h H = mVH T
Assertion mvhf1 T mFS H : V 1-1 E

Proof

Step Hyp Ref Expression
1 mvhf.v V = mVR T
2 mvhf.e E = mEx T
3 mvhf.h H = mVH T
4 1 2 3 mvhf T mFS H : V E
5 eqid mType T = mType T
6 1 5 3 mvhval v V H v = mType T v ⟨“ v ”⟩
7 1 5 3 mvhval w V H w = mType T w ⟨“ w ”⟩
8 6 7 eqeqan12d v V w V H v = H w mType T v ⟨“ v ”⟩ = mType T w ⟨“ w ”⟩
9 8 adantl T mFS v V w V H v = H w mType T v ⟨“ v ”⟩ = mType T w ⟨“ w ”⟩
10 fvex mType T v V
11 s1cli ⟨“ v ”⟩ Word V
12 11 elexi ⟨“ v ”⟩ V
13 10 12 opth mType T v ⟨“ v ”⟩ = mType T w ⟨“ w ”⟩ mType T v = mType T w ⟨“ v ”⟩ = ⟨“ w ”⟩
14 13 simprbi mType T v ⟨“ v ”⟩ = mType T w ⟨“ w ”⟩ ⟨“ v ”⟩ = ⟨“ w ”⟩
15 s111 v V w V ⟨“ v ”⟩ = ⟨“ w ”⟩ v = w
16 15 adantl T mFS v V w V ⟨“ v ”⟩ = ⟨“ w ”⟩ v = w
17 14 16 syl5ib T mFS v V w V mType T v ⟨“ v ”⟩ = mType T w ⟨“ w ”⟩ v = w
18 9 17 sylbid T mFS v V w V H v = H w v = w
19 18 ralrimivva T mFS v V w V H v = H w v = w
20 dff13 H : V 1-1 E H : V E v V w V H v = H w v = w
21 4 19 20 sylanbrc T mFS H : V 1-1 E