Metamath Proof Explorer


Theorem nqex

Description: The class of positive fractions exists. (Contributed by NM, 16-Aug-1995) (Revised by Mario Carneiro, 27-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion nqex
|- Q. e. _V

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 niex
 |-  N. e. _V
3 2 2 xpex
 |-  ( N. X. N. ) e. _V
4 1 3 rabex2
 |-  Q. e. _V