Definition df-1st 3087

Description: Define a function that extracts the first member of an ordered pair. Equivalent to Definition 5.13 (i) of [Monk1] p. 52 (compare op1stb 1992 and op1sta 2635).

Assertion

Ref	Expression
df-1st	⊢ 1st = {⟨x, y⟩∣y = ∪dom {x}}

Distinct variable group(s):   x,y

Detailed syntax breakdown of Definition df-1st

Step	Hyp	Ref	Expression
1		c1st 3085	. 2 class 1st
2		vy	. . . . 5 set y
3	2	cv 1089	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 1089	. . . . . . 7 class x
6	5	csn 1808	. . . . . 6 class {x}
7	6	cdm 2410	. . . . 5 class dom {x}
8	7	cuni 1919	. . . 4 class ∪dom {x}
9	3, 8	wceq 1091	. . 3 wff y = ∪dom {x}
10	9, 4, 2	copab 2055	. 2 class {⟨x, y⟩∣y = ∪dom {x}}
11	1, 10	wceq 1091	1 wff 1st = {⟨x, y⟩∣y = ∪dom {x}}

This definition is referenced by:  1stval 3089  fo1st 3094  f1stres 3096

metamath.org