NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-proj1 Unicode 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 Phi
Distinct variable group:   ,

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