Definition df-evenfin 4445

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

Step	Hyp	Ref	Expression
1		cevenfin 4437	. 2 class Evenfin
2		vx	. . . . . . 7 setvar x
3	2	cv 1641	. . . . . 6 class x
4		vn	. . . . . . . 8 setvar n
5	4	cv 1641	. . . . . . 7 class n
6	5, 5	cplc 4376	. . . . . 6 class (n +c n)
7	3, 6	wceq 1642	. . . . 5 wff x = (n +c n)
8		cnnc 4374	. . . . 5 class Nn
9	7, 4, 8	wrex 2616	. . . 4 wff ∃n ∈ Nn x = (n +c n)
10		c0 3551	. . . . 5 class ∅
11	3, 10	wne 2517	. . . 4 wff x ≠ ∅
12	9, 11	wa 358	. . 3 wff (∃n ∈ Nn x = (n +c n) ∧ x ≠ ∅)
13	12, 2	cab 2339	. 2 class {x ∣ (∃n ∈ Nn x = (n +c n) ∧ x ≠ ∅)}
14	1, 13	wceq 1642	1 wff Evenfin = {x ∣ (∃n ∈ Nn x = (n +c n) ∧ x ≠ ∅)}

This definition is referenced by:  evenfinex  4504  0ceven  4506  evennn  4507  evennnul  4509  sucevenodd  4511  sucoddeven  4512  dfevenfin2  4513  eventfin  4518