Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-proj2 | Unicode version | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-proj2 |
 Proj2       Phi  0c   |
,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | 1 | cproj2 4564 |
. 2
Proj2 |
| 3 | vx |
. . . . . . 7
 | |
| 4 | 3 | cv 1641 |
. . . . . 6
|
| 5 | 4 | cphi 4562 |
. . . . 5
Phi |
| 6 | c0c 4374 |
. . . . . 6
0c | |
| 7 | 6 | csn 3737 |
. . . . 5
0c |
| 8 | 5, 7 | cun 3207 |
. . . 4
Phi
0c |
| 9 | 8, 1 | wcel 1710 |
. . 3
 Phi 0c |
| 10 | 9, 3 | cab 2339 |
. 2
Phi 0c |
| 11 | 2, 10 | wceq 1642 |
1
Proj2 Phi 0c |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfproj22 4577 proj2op 4601 opeq 4619 |
| Copyright terms: Public domain | W3C validator |