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

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