Definition df-q 4628

Description: Define the set of rationals. Definition of rational numbers in [Apostol] p. 22.

Assertion

Ref	Expression
df-q	⊢ ℚ = {x∣∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-q

Step	Hyp	Ref	Expression
1		cq 4096	. 2 class ℚ
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		vy	. . . . . . . 8 set y
5	4	cv 1089	. . . . . . 7 class y
6		vz	. . . . . . . 8 set z
7	6	cv 1089	. . . . . . 7 class z
8		cdiv 4091	. . . . . . 7 class /
9	5, 7, 8	co 3001	. . . . . 6 class (y / z)
10	3, 9	wceq 1091	. . . . 5 wff x = (y / z)
11		cn 4093	. . . . 5 class ℕ
12	10, 6, 11	wrex 1202	. . . 4 wff ∃z ∈ ℕ x = (y / z)
13		cz 4095	. . . 4 class ℤ
14	12, 4, 13	wrex 1202	. . 3 wff ∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)
15	14, 2	cab 1090	. 2 class {x∣∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)}
16	1, 15	wceq 1091	1 wff ℚ = {x∣∃y ∈ ℤ ∃z ∈ ℕ x = (y / z)}

This definition is referenced by:  elq 4629

metamath.org