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 = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2nd	⊢ 2nd
1		vx	⊢ 𝑥
2		cvv	⊢ V
3	1	cv	⊢ 𝑥
4	3	csn	⊢ { 𝑥 }
5	4	crn	⊢ ran { 𝑥 }
6	5	cuni	⊢ ∪ ran { 𝑥 }
7	1 2 6	cmpt	⊢ ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
8	0 7	wceq	⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )