Definition df-1st 4724

Description: Define a function that extracts the first member, or abscissa, of an ordered pair. (Contributed by SF, 5-Jan-2015.)

Assertion

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

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-1st

Step	Hyp	Ref	Expression
1		c1st 4718	. 2 class 1st
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4		vy	. . . . . . 7 setvar y
5	4	cv 1641	. . . . . 6 class y
6		vz	. . . . . . 7 setvar z
7	6	cv 1641	. . . . . 6 class z
8	5, 7	cop 4562	. . . . 5 class ⟨y, z⟩
9	3, 8	wceq 1642	. . . 4 wff x = ⟨y, z⟩
10	9, 6	wex 1541	. . 3 wff ∃z x = ⟨y, z⟩
11	10, 2, 4	copab 4623	. 2 class {⟨x, y⟩ ∣ ∃z x = ⟨y, z⟩}
12	1, 11	wceq 1642	1 wff 1st = {⟨x, y⟩ ∣ ∃z x = ⟨y, z⟩}

This definition is referenced by:  el1st  4730  df1st2  4739  br1st  4859