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

Definition df-proj2 4568
Description: Define the second projection operation. This operation recovers the second element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Assertion
Ref Expression
df-proj2 Proj2 A = {x ( Phi x ∪ {0c}) A}
Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-proj2
StepHypRef Expression
1 cA . . 3 class A
21cproj2 4564 . 2 class Proj2 A
3 vx . . . . . . 7 setvar x
43cv 1641 . . . . . 6 class x
54cphi 4562 . . . . 5 class Phi x
6 c0c 4374 . . . . . 6 class 0c
76csn 3737 . . . . 5 class {0c}
85, 7cun 3207 . . . 4 class ( Phi x ∪ {0c})
98, 1wcel 1710 . . 3 wff ( Phi x ∪ {0c}) A
109, 3cab 2339 . 2 class {x ( Phi x ∪ {0c}) A}
112, 10wceq 1642 1 wff Proj2 A = {x ( Phi x ∪ {0c}) A}
Colors of variables: wff setvar class
This definition is referenced by:  dfproj22  4577  proj2op  4601  opeq  4619
  Copyright terms: Public domain W3C validator