Definition df-proj1 4568

Description: Define the first projection operation. This operation recovers the first element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)

Assertion

Ref	Expression
df-proj1	|- Proj1 A = {x | Phi x e. A}

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-proj1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cproj1 4564	. 2 class Proj1 A
3		vx	. . . . . 6 setvar x
4	3	cv 1641	. . . . 5 class x
5	4	cphi 4563	. . . 4 class Phi x
6	5, 1	wcel 1710	. . 3 wff Phi x e. A
7	6, 3	cab 2339	. 2 class {x | Phi x e. A}
8	2, 7	wceq 1642	1 wff Proj1 A = {x | Phi x e. A}

This definition is referenced by:  dfproj12  4577  proj1op  4601  opeq  4620