Definition df-q 6194

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 5271	. 2 class QQ
2		vx	. . . . . . 7 set x
3	2	cv 952	. . . . . 6 class x
4		vm	. . . . . . . 8 set m
5	4	cv 952	. . . . . . 7 class m
6		vn	. . . . . . . 8 set n
7	6	cv 952	. . . . . . 7 class n
8		cdiv 5266	. . . . . . 7 class /
9	5, 7, 8	co 3948	. . . . . 6 class (m / n)
10	3, 9	wceq 953	. . . . 5 wff x = (m / n)
11		cn 5268	. . . . 5 class NN
12	10, 6, 11	wrex 1638	. . . 4 wff E.n e. NN x = (m / n)
13		cz 5270	. . . 4 class ZZ
14	12, 4, 13	wrex 1638	. . 3 wff E.m e. ZZ E.n e. NN x = (m / n)
15	14, 2	cab 1456	. 2 class {x | E.m e. ZZ E.n e. NN x = (m / n)}
16	1, 15	wceq 953	1 wff QQ = {x | E.m e. ZZ E.n e. NN x = (m / n)}

This definition is referenced by:  elq 6195

Copyright terms: Public domain