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

Definition df-oddfin 4445
Description: Define the temporary set of all odd numbers. This differs from the final definition due to the non-null condition. Definition from [Rosser] p. 529. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-oddfin Oddfin Nn 1c
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-oddfin
StepHypRef Expression
1 coddfin 4437 . 2 Oddfin
2 vx . . . . . . 7
32cv 1641 . . . . . 6
4 vn . . . . . . . . 9
54cv 1641 . . . . . . . 8
65, 5cplc 4375 . . . . . . 7
7 c1c 4134 . . . . . . 7 1c
86, 7cplc 4375 . . . . . 6 1c
93, 8wceq 1642 . . . . 5 1c
10 cnnc 4373 . . . . 5 Nn
119, 4, 10wrex 2615 . . . 4 Nn 1c
12 c0 3550 . . . . 5
133, 12wne 2516 . . . 4
1411, 13wa 358 . . 3 Nn 1c
1514, 2cab 2339 . 2 Nn 1c
161, 15wceq 1642 1 Oddfin Nn 1c
Colors of variables: wff setvar class
This definition is referenced by:  oddfinex  4504  oddnn  4507  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  dfoddfin2  4513  oddtfin  4518
  Copyright terms: Public domain W3C validator