Description: The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 27-Apr-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 0nnq | |- -. (/) e. Q. |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0nelxp | |- -. (/) e. ( N. X. N. ) |
|
2 | df-nq | |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) |
|
3 | 2 | ssrab3 | |- Q. C_ ( N. X. N. ) |
4 | 3 | sseli | |- ( (/) e. Q. -> (/) e. ( N. X. N. ) ) |
5 | 1 4 | mto | |- -. (/) e. Q. |