This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ℚ = \div [ℤ \times ℕ]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cq	$class ℚ$
1		cdiv	$class \div$
2		cz	$class ℤ$
3		cn	$class ℕ$
4	2 3	cxp	$class (ℤ \times ℕ)$
5	1 4	cima	$class \div [ℤ \times ℕ]$
6	0 5	wceq	$wff ℚ = \div [ℤ \times ℕ]$