Metamath Proof Explorer


Theorem 1stval2

Description: Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

Ref Expression
Assertion 1stval2 A V × V 1 st A = A

Proof

Step Hyp Ref Expression
1 elvv A V × V x y A = x y
2 vex x V
3 vex y V
4 2 3 op1st 1 st x y = x
5 2 3 op1stb x y = x
6 4 5 eqtr4i 1 st x y = x y
7 fveq2 A = x y 1 st A = 1 st x y
8 inteq A = x y A = x y
9 8 inteqd A = x y A = x y
10 6 7 9 3eqtr4a A = x y 1 st A = A
11 10 exlimivv x y A = x y 1 st A = A
12 1 11 sylbi A V × V 1 st A = A