Description: Each positive fraction is an ordered pair of positive integers (the numerator and denominator, in "lowest terms". (Contributed by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elpqn | |- ( A e. Q. -> A e. ( N. X. N. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-nq | |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) |
|
| 2 | 1 | ssrab3 | |- Q. C_ ( N. X. N. ) |
| 3 | 2 | sseli | |- ( A e. Q. -> A e. ( N. X. N. ) ) |