Definition df-z 6083

Description: Define the set of integers. Definition of integers in [Apostol] p. 22.

Assertion

Ref	Expression
df-z	|- ZZ = {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}

Detailed syntax breakdown of Definition df-z

Step	Hyp	Ref	Expression
1		cz 5270	. 2 class ZZ
2		vn	. . . . . 6 set n
3	2	cv 952	. . . . 5 class n
4		cc0 5206	. . . . 5 class 0
5	3, 4	wceq 953	. . . 4 wff n = 0
6		cn 5268	. . . . 5 class NN
7	3, 6	wcel 955	. . . 4 wff n e. NN
8	3	cneg 5265	. . . . 5 class -un
9	8, 6	wcel 955	. . . 4 wff -un e. NN
10	5, 7, 9	w3o 772	. . 3 wff (n = 0 \/ n e. NN \/ -un e. NN)
11		cr 5205	. . 3 class RR
12	10, 2, 11	crab 1640	. 2 class {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}
13	1, 12	wceq 953	1 wff ZZ = {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}

This definition is referenced by:  elz 6084

Copyright terms: Public domain