Metamath Proof Explorer


Theorem elpqn

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

Proof

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