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 |