Definition df-1st 5020

Description: Define a function that extracts the first member, or abscissa, of an ordered pair. Theorem op1st 5026 proves that it does this. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1sta 4372 and op1stb 3857). The notation is the same as Monk's.

Assertion

Ref	Expression
df-1st	|- 1st = {<.x, y>. | y = U.dom { x}}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-1st

Step	Hyp	Ref	Expression
1		c1st 5018	. 2 class 1st
2		vy	. . . . 5 set y
3	2	cv 1297	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 1297	. . . . . . 7 class x
6	5	csn 3044	. . . . . 6 class {x}
7	6	cdm 3986	. . . . 5 class dom { x}
8	7	cuni 3177	. . . 4 class U.dom { x}
9	3, 8	wceq 1298	. . 3 wff y = U.dom { x}
10	9, 4, 2	copab 3395	. 2 class {<.x, y>. | y = U.dom { x}}
11	1, 10	wceq 1298	1 wff 1st = {<.x, y>. | y = U.dom { x}}

This definition is referenced by:  1stval 5022  fo1st 5032  f1stres 5034

Copyright terms: Public domain