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