Metamath Proof Explorer

Definition df-2nd

Description: Define a function that extracts the second member, or ordinate, of an ordered pair. Theorem op2nd proves that it does this. For example, ( 2nd<. 3 , 4 >. ) = 4 . Equivalent to Definition 5.13 (ii) of Monk1 p. 52 (compare op2nda and op2ndb ). The notation is the same as Monk's. (Contributed by NM, 9-Oct-2004)

Ref Expression
Assertion df-2nd 
|- 2nd = ( x e. _V |-> U. ran { x } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c2nd 
 |-  2nd
1 vx 
 |-  x
2 cvv 
 |-  _V
3 1 cv 
 |-  x
4 3 csn 
 |-  { x }
5 4 crn 
 |-  ran { x }
6 5 cuni 
 |-  U. ran { x }
7 1 2 6 cmpt 
 |-  ( x e. _V |-> U. ran { x } )
8 0 7 wceq 
 |-  2nd = ( x e. _V |-> U. ran { x } )