Definition df-oddfin 4446

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

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

This definition is referenced by:  oddfinex  4505  oddnn  4508  oddnnul  4510  sucevenodd  4511  sucoddeven  4512  dfoddfin2  4514  oddtfin  4519