Theorem op2nda

Description: Extract the second member of an ordered pair. (See op1sta to extract the first member, op2ndb for an alternate version, and op2nd for the preferred version.) (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Hypotheses	cnvsn.1	|- A e. _V
	cnvsn.2	|- B e. _V
Assertion	op2nda	|- U. ran { <. A , B >. } = B

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	|- A e. _V
2		cnvsn.2	|- B e. _V
3	1	rnsnop	|- ran { <. A , B >. } = { B }
4	3	unieqi	|- U. ran { <. A , B >. } = U. { B }
5	2	unisn	|- U. { B } = B
6	4 5	eqtri	|- U. ran { <. A , B >. } = B