Metamath Proof Explorer

Theorem op1stg

Description: Extract the first member of an ordered pair. (Contributed by NM, 19-Jul-2005)

Ref Expression
Assertion op1stg 
|- ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )

Proof

Step Hyp Ref Expression
1 opeq1 
 |-  ( x = A -> <. x , y >. = <. A , y >. )
2 1 fveq2d 
 |-  ( x = A -> ( 1st ` <. x , y >. ) = ( 1st ` <. A , y >. ) )
3 id 
 |-  ( x = A -> x = A )
4 2 3 eqeq12d 
 |-  ( x = A -> ( ( 1st ` <. x , y >. ) = x <-> ( 1st ` <. A , y >. ) = A ) )
5 opeq2 
 |-  ( y = B -> <. A , y >. = <. A , B >. )
6 5 fveqeq2d 
 |-  ( y = B -> ( ( 1st ` <. A , y >. ) = A <-> ( 1st ` <. A , B >. ) = A ) )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 op1st 
 |-  ( 1st ` <. x , y >. ) = x
10 4 6 9 vtocl2g 
 |-  ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )