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	⊢ ℚ = ( / “ ( ℤ × ℕ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cq	⊢ ℚ
1		cdiv	⊢ /
2		cz	⊢ ℤ
3		cn	⊢ ℕ
4	2 3	cxp	⊢ ( ℤ × ℕ )
5	1 4	cima	⊢ ( / “ ( ℤ × ℕ ) )
6	0 5	wceq	⊢ ℚ = ( / “ ( ℤ × ℕ ) )