Definition df-q 7436

Description: Define the set of rational numbers. Definition of rationals in [Apostol] p. 22.

Assertion

Ref	Expression
df-q	|- QQ = {x | E.m e. ZZ E.n e. NN x = (m / n)}

Distinct variable group:   m,n,x

Detailed syntax breakdown of Definition df-q

Step	Hyp	Ref	Expression
1		cq 6452	. 2 class QQ
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		vm	. . . . . . . 8 set m
5	4	cv 1297	. . . . . . 7 class m
6		vn	. . . . . . . 8 set n
7	6	cv 1297	. . . . . . 7 class n
8		cdiv 6447	. . . . . . 7 class /
9	5, 7, 8	co 4884	. . . . . 6 class (m / n)
10	3, 9	wceq 1298	. . . . 5 wff x = (m / n)
11		cn 6449	. . . . 5 class NN
12	10, 6, 11	wrex 2106	. . . 4 wff E.n e. NN x = (m / n)
13		cz 6451	. . . 4 class ZZ
14	12, 4, 13	wrex 2106	. . 3 wff E.m e. ZZ E.n e. NN x = (m / n)
15	14, 2	cab 1871	. 2 class {x | E.m e. ZZ E.n e. NN x = (m / n)}
16	1, 15	wceq 1298	1 wff QQ = {x | E.m e. ZZ E.n e. NN x = (m / n)}

This definition is referenced by:  elq 7437

Copyright terms: Public domain