Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31Aug2015)
Ref  Expression  

Hypotheses  op1st.1   A e. _V 

op1st.2   B e. _V 

Assertion  op2ndd   ( C = <. A , B >. > ( 2nd ` C ) = B ) 
Step  Hyp  Ref  Expression 

1  op1st.1   A e. _V 

2  op1st.2   B e. _V 

3  fveq2   ( C = <. A , B >. > ( 2nd ` C ) = ( 2nd ` <. A , B >. ) ) 

4  1 2  op2nd   ( 2nd ` <. A , B >. ) = B 
5  3 4  eqtrdi   ( C = <. A , B >. > ( 2nd ` C ) = B ) 