This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0pss

Description: The null set is a proper subset of any nonempty set. (Contributed by NM, 27-Feb-1996)

Ref Expression
Assertion 0pss ⊢ ∅ ⊂ A ↔ A ≠ ∅

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ A
2 df-pss ⊢ ∅ ⊂ A ↔ ∅ ⊆ A ∧ ∅ ≠ A
3 1 2 mpbiran ⊢ ∅ ⊂ A ↔ ∅ ≠ A
4 necom ⊢ ∅ ≠ A ↔ A ≠ ∅
5 3 4 bitri ⊢ ∅ ⊂ A ↔ A ≠ ∅