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

Metamath Proof Explorer

Theorem 0sn0ep

Description: An example for the membership relation. (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion 0sn0ep ⊢ ∅ E ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 snid ⊢ ∅ ∈ ∅
3 snex ⊢ ∅ ∈ V
4 3 epeli ⊢ ∅ E ∅ ↔ ∅ ∈ ∅
5 2 4 mpbir ⊢ ∅ E ∅