Metamath Proof Explorer


Theorem 0npr

Description: The empty set is not a positive real. (Contributed by NM, 15-Nov-1995) (New usage is discouraged.)

Ref Expression
Assertion 0npr ¬ ∅ ∈ P

Proof

Step Hyp Ref Expression
1 eqid ∅ = ∅
2 prn0 ( ∅ ∈ P → ∅ ≠ ∅ )
3 2 necon2bi ( ∅ = ∅ → ¬ ∅ ∈ P )
4 1 3 ax-mp ¬ ∅ ∈ P