Definition df-q

Description: Define the set of rational numbers. Based on definition of rationals in Apostol p. 22. See elq for the relation "is rational". (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	df-q	$$⊢\mathbb{Q}=÷\left[\mathbb{Z}\times \mathbb{N}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cq	$$class\mathbb{Q}$$
1		cdiv	$$class÷$$
2		cz	$$class\mathbb{Z}$$
3		cn	$$class\mathbb{N}$$
4	2 3	cxp	$$class\left(\mathbb{Z}\times \mathbb{N}\right)$$
5	1 4	cima	$$class÷\left[\mathbb{Z}\times \mathbb{N}\right]$$
6	0 5	wceq	$$wff\mathbb{Q}=÷\left[\mathbb{Z}\times \mathbb{N}\right]$$