Definition df-2nd 4070

Description: Define a function that extracts the second member of an ordered pair. Theorem op2nd 4076 proves that it does this. Equivalent to Definition 5.13 (ii) of [Monk1] p. 52 (compare op2nda 3444 and op2ndb 3443). The notation is the same as Monk's.

Assertion

Ref	Expression
df-2nd	|- 2nd = {<.x, y>. | y = U.ran { x}}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-2nd

Step	Hyp	Ref	Expression
1		c2nd 4068	. 2 class 2nd
2		vy	. . . . 5 set y
3	2	cv 953	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 953	. . . . . . 7 class x
6	5	csn 2405	. . . . . 6 class {x}
7	6	crn 3166	. . . . 5 class ran { x}
8	7	cuni 2498	. . . 4 class U.ran { x}
9	3, 8	wceq 954	. . 3 wff y = U.ran { x}
10	9, 4, 2	copab 2661	. 2 class {<.x, y>. | y = U.ran { x}}
11	1, 10	wceq 954	1 wff 2nd = {<.x, y>. | y = U.ran { x}}

This definition is referenced by:  2ndval 4072  fo2nd 4082  f2ndres 4084

Copyright terms: Public domain