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. ) ) |