Theorem elq 6309

Description: Membership in the set of rationals.

Assertion

Ref	Expression
elq	⊢ (A ∈ ℚ ↔ ∃x ∈ ℤ ∃y ∈ ℕ A = (x / y))

Distinct variable group:   x,y,A

Proof of Theorem elq

Step	Hyp	Ref	Expression
1		df-q 6308	. . 3 ⊢ ℚ = {z∣∃x ∈ ℤ ∃y ∈ ℕ z = (x / y)}
2	1	eleq2i 1585	. 2 ⊢ (A ∈ ℚ ↔ A ∈ {z∣∃x ∈ ℤ ∃y ∈ ℕ z = (x / y)})
3		oprex 4041	. . . . . . . 8 ⊢ (x / y) ∈ V
4		eleq1 1581	. . . . . . . 8 ⊢ (A = (x / y) → (A ∈ V ↔ (x / y) ∈ V))
5	3, 4	mpbiri 201	. . . . . . 7 ⊢ (A = (x / y) → A ∈ V)
6	5	a1i 8	. . . . . 6 ⊢ (y ∈ ℕ → (A = (x / y) → A ∈ V))
7	6	r19.23aiv 1790	. . . . 5 ⊢ (∃y ∈ ℕ A = (x / y) → A ∈ V)
8	7	a1i 8	. . . 4 ⊢ (x ∈ ℤ → (∃y ∈ ℕ A = (x / y) → A ∈ V))
9	8	r19.23aiv 1790	. . 3 ⊢ (∃x ∈ ℤ ∃y ∈ ℕ A = (x / y) → A ∈ V)
10		eqeq1 1528	. . . 4 ⊢ (z = A → (z = (x / y) ↔ A = (x / y)))
11	10	2rexbidv 1728	. . 3 ⊢ (z = A → (∃x ∈ ℤ ∃y ∈ ℕ z = (x / y) ↔ ∃x ∈ ℤ ∃y ∈ ℕ A = (x / y)))
12	9, 11	elab3 1950	. 2 ⊢ (A ∈ {z∣∃x ∈ ℤ ∃y ∈ ℕ z = (x / y)} ↔ ∃x ∈ ℤ ∃y ∈ ℕ A = (x / y))
13	2, 12	bitri 180	1 ⊢ (A ∈ ℚ ↔ ∃x ∈ ℤ ∃y ∈ ℕ A = (x / y))

Syntax hints:   → wi 3   ↔ wb 153   = wceq 997   ∈ wcel 999  {cab 1509  ∃wrex 1693  Vcvv 1858  (class class class)co 4021   / cdiv 5359  ℕcn 5361  ℤcz 5363  ℚcq 5364

This theorem is referenced by:  znq 6310  qre 6311  zq 6312  qaddcl 6321  qnegcl 6322  qmulcl 6323  qreccl 6325  sqr2irr 6819  eirr 7484  qnnen 7595  ipasslem5 8578

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-uni 2558  df-fv 3255  df-opr 4023  df-q 6308

Copyright terms: Public domain