NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-oddfin GIF 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 = {x (n Nn x = ((n +c n) +c 1c) x)}
Distinct variable group:   x,n

Detailed syntax breakdown of Definition df-oddfin
StepHypRef Expression
1 coddfin 4437 . 2 class Oddfin
2 vx . . . . . . 7 setvar x
32cv 1641 . . . . . 6 class x
4 vn . . . . . . . . 9 setvar n
54cv 1641 . . . . . . . 8 class n
65, 5cplc 4375 . . . . . . 7 class (n +c n)
7 c1c 4134 . . . . . . 7 class 1c
86, 7cplc 4375 . . . . . 6 class ((n +c n) +c 1c)
93, 8wceq 1642 . . . . 5 wff x = ((n +c n) +c 1c)
10 cnnc 4373 . . . . 5 class Nn
119, 4, 10wrex 2615 . . . 4 wff n Nn x = ((n +c n) +c 1c)
12 c0 3550 . . . . 5 class
133, 12wne 2516 . . . 4 wff x
1411, 13wa 358 . . 3 wff (n Nn x = ((n +c n) +c 1c) x)
1514, 2cab 2339 . 2 class {x (n Nn x = ((n +c n) +c 1c) x)}
161, 15wceq 1642 1 wff Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
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