NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-proj1 GIF version

Definition df-proj1 4567
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 A}
Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-proj1
StepHypRef Expression
1 cA . . 3 class A
21cproj1 4563 . 2 class Proj1 A
3 vx . . . . . 6 setvar x
43cv 1641 . . . . 5 class x
54cphi 4562 . . . 4 class Phi x
65, 1wcel 1710 . . 3 wff Phi x A
76, 3cab 2339 . 2 class {x Phi x A}
82, 7wceq 1642 1 wff Proj1 A = {x Phi x A}
Colors of variables: wff setvar class
This definition is referenced by:  dfproj12  4576  proj1op  4600  opeq  4619
  Copyright terms: Public domain W3C validator