This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )

Proof

Step Hyp Ref Expression
1 elvv 
 |-  ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 op1st 
 |-  ( 1st ` <. x , y >. ) = x
5 2 3 op1stb 
 |-  |^| |^| <. x , y >. = x
6 4 5 eqtr4i 
 |-  ( 1st ` <. x , y >. ) = |^| |^| <. x , y >.
7 fveq2 
 |-  ( A = <. x , y >. -> ( 1st ` A ) = ( 1st ` <. 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 >. -> ( 1st ` A ) = |^| |^| A )
11 10 exlimivv 
 |-  ( E. x E. y A = <. x , y >. -> ( 1st ` A ) = |^| |^| A )
12 1 11 sylbi 
 |-  ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )