Theorem op2ndd

Description: Extract the second member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	op1st.1	|- A e. _V
	op1st.2	|- B e. _V
Assertion	op2ndd	|- ( C = <. A , B >. -> ( 2nd ` C ) = B )

Proof

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 )