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

Metamath Proof Explorer

Theorem epn0

Description: The membership relation is nonempty. (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion epn0 ⊢ E ≠ ∅

Proof

Step Hyp Ref Expression
1 0sn0ep ⊢ ∅ E ∅
2 brne0 ⊢ ∅ E ∅ → E ≠ ∅
3 1 2 ax-mp ⊢ E ≠ ∅