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

Detailed syntax breakdown of Definition df-evenfin
StepHypRef Expression
1 cevenfin 4436 . 2 class Evenfin
2 vx . . . . . . 7 setvar x
32cv 1641 . . . . . 6 class x
4 vn . . . . . . . 8 setvar n
54cv 1641 . . . . . . 7 class n
65, 5cplc 4375 . . . . . 6 class (n +c n)
73, 6wceq 1642 . . . . 5 wff x = (n +c n)
8 cnnc 4373 . . . . 5 class Nn
97, 4, 8wrex 2615 . . . 4 wff n Nn x = (n +c n)
10 c0 3550 . . . . 5 class
113, 10wne 2516 . . . 4 wff x
129, 11wa 358 . . 3 wff (n Nn x = (n +c n) x)
1312, 2cab 2339 . 2 class {x (n Nn x = (n +c n) x)}
141, 13wceq 1642 1 wff Evenfin = {x (n Nn x = (n +c n) x)}
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