Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-spfin | Unicode version | ||
| Description: Define the finite Sp set. Definition from [Rosser] p. 533. (Contributed by SF, 12-Jan-2015.) |
| Ref | Expression |
|---|---|
| df-spfin |
 Spfin       Ncfin  
![](wedge.gif "/\"){kind=small}  
 Sfin   
 |
,,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cspfin 4439 |
. 2
 Spfin | |
| 2 | cvv 2859 |
. . . . . . 7
| |
| 3 | 2 | cncfin 4434 |
. . . . . 6
Ncfin |
| 4 | va |
. . . . . . 7
 | |
| 5 | 4 | cv 1641 |
. . . . . 6
|
| 6 | 3, 5 | wcel 1710 |
. . . . 5
 Ncfin |
| 7 | vz |
. . . . . . . . . 10
| |
| 8 | 7 | cv 1641 |
. . . . . . . . 9
|
| 9 | vx |
. . . . . . . . . 10
| |
| 10 | 9 | cv 1641 |
. . . . . . . . 9
|
| 11 | 8, 10 | wsfin 4438 |
. . . . . . . 8
Sfin |
| 12 | 7, 4 | wel 1711 |
. . . . . . . 8
|
| 13 | 11, 12 | wi 4 |
. . . . . . 7
Sfin |
| 14 | 13, 7 | wal 1540 |
. . . . . 6
Sfin
|
| 15 | 14, 9, 5 | wral 2614 |
. . . . 5
Sfin
|
| 16 | 6, 15 | wa 358 |
. . . 4
Ncfin
Sfin |
| 17 | 16, 4 | cab 2339 |
. . 3
Ncfin
Sfin |
| 18 | 17 | cint 3926 |
. 2
Ncfin
Sfin |
| 19 | 1, 18 | wceq 1642 |
1
Spfin Ncfin
Sfin
|
| Colors of variables: wff setvar class |
| This definition is referenced by: spfinex 4537 ncvspfin 4538 spfinsfincl 4539 spfininduct 4540 |
| Copyright terms: Public domain | W3C validator |