Metamath Proof Explorer

Theorem op2ndg

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

Ref Expression
Assertion op2ndg 
|- ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )

Proof

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