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

Definition df-evenfin 4444
Description: Define the temporary set of all even 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-evenfin Evenfin Nn
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-evenfin
StepHypRef Expression
1 cevenfin 4436 . 2 Evenfin
2 vx . . . . . . 7
32cv 1641 . . . . . 6
4 vn . . . . . . . 8
54cv 1641 . . . . . . 7
65, 5cplc 4375 . . . . . 6
73, 6wceq 1642 . . . . 5
8 cnnc 4373 . . . . 5 Nn
97, 4, 8wrex 2615 . . . 4 Nn
10 c0 3550 . . . . 5
113, 10wne 2516 . . . 4
129, 11wa 358 . . 3 Nn
1312, 2cab 2339 . 2 Nn
141, 13wceq 1642 1 Evenfin Nn
Colors of variables: wff setvar class
This definition is referenced by:  evenfinex  4503  0ceven  4505  evennn  4506  evennnul  4508  sucevenodd  4510  sucoddeven  4511  dfevenfin2  4512  eventfin  4517
  Copyright terms: Public domain W3C validator