Definition df-q 7894

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 7097	. 2 class QQ
2		vx	. . . . . . 7 set x
3	2	cv 1614	. . . . . 6 class x
4		vm	. . . . . . . 8 set m
5	4	cv 1614	. . . . . . 7 class m
6		vn	. . . . . . . 8 set n
7	6	cv 1614	. . . . . . 7 class n
8		cdiv 7093	. . . . . . 7 class /
9	5, 7, 8	co 5020	. . . . . 6 class (m / n)
10	3, 9	wceq 1615	. . . . 5 wff x = (m / n)
11		cn 7094	. . . . 5 class NN
12	10, 6, 11	wrex 2386	. . . 4 wff E.n e. NN x = (m / n)
13		cz 7096	. . . 4 class ZZ
14	12, 4, 13	wrex 2386	. . 3 wff E.m e. ZZ E.n e. NN x = (m / n)
15	14, 2	cab 2157	. 2 class {x | E.m e. ZZ E.n e. NN x = (m / n)}
16	1, 15	wceq 1615	1 wff QQ = {x | E.m e. ZZ E.n e. NN x = (m / n)}

This definition is referenced by:  elq 7895

Copyright terms: Public domain