Theorem op2nd

Description: Extract the second member of an ordered pair. (Contributed by NM, 5-Oct-2004)

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

Proof

Step	Hyp	Ref	Expression
1		op1st.1	|- A e. _V
2		op1st.2	|- B e. _V
3		2ndval	|- ( 2nd ` <. A , B >. ) = U. ran { <. A , B >. }
4	1 2	op2nda	|- U. ran { <. A , B >. } = B
5	3 4	eqtri	|- ( 2nd ` <. A , B >. ) = B