Definition df-z 6091

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 5278	. 2 class ZZ
2		vn	. . . . . 6 set n
3	2	cv 953	. . . . 5 class n
4		cc0 5214	. . . . 5 class 0
5	3, 4	wceq 954	. . . 4 wff n = 0
6		cn 5276	. . . . 5 class NN
7	3, 6	wcel 956	. . . 4 wff n e. NN
8	3	cneg 5273	. . . . 5 class -un
9	8, 6	wcel 956	. . . 4 wff -un e. NN
10	5, 7, 9	w3o 773	. . 3 wff (n = 0 \/ n e. NN \/ -un e. NN)
11		cr 5213	. . 3 class RR
12	10, 2, 11	crab 1645	. 2 class {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}
13	1, 12	wceq 954	1 wff ZZ = {n e. RR | (n = 0 \/ n e. NN \/ -un e. NN)}

This definition is referenced by:  elz 6092

Copyright terms: Public domain