Definition df-2nd 4797

Description: Define the 2nd function. This function extracts the second member of an ordered pair. (Contributed by SF, 5-Jan-2015.)

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-2nd

Step	Hyp	Ref	Expression
1		c2nd 4783	. 2 class 2nd
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4		vz	. . . . . . 7 setvar z
5	4	cv 1641	. . . . . 6 class z
6		vy	. . . . . . 7 setvar y
7	6	cv 1641	. . . . . 6 class y
8	5, 7	cop 4561	. . . . 5 class <.z, y>.
9	3, 8	wceq 1642	. . . 4 wff x = <.z, y>.
10	9, 4	wex 1541	. . 3 wff E.z x = <.z, y>.
11	10, 2, 6	copab 4622	. 2 class {<.x, y>. | E.z x = <.z, y>.}
12	1, 11	wceq 1642	1 wff 2nd = {<.x, y>. | E.z x = <.z, y>.}

This definition is referenced by:  br2nd  4859  df2nd2  5111