This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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