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

Metamath Proof Explorer

Theorem vtxval0

Description: Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020)

Ref Expression
Assertion vtxval0 ⊢ Vtx ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0nelxp ⊢ ¬ ∅ ∈ V × V
2 1 iffalsei ⊢ if ∅ ∈ V × V 1 st ⁡ ∅ Base ∅ = Base ∅
3 vtxval ⊢ Vtx ⁡ ∅ = if ∅ ∈ V × V 1 st ⁡ ∅ Base ∅
4 base0 ⊢ ∅ = Base ∅
5 2 3 4 3eqtr4i ⊢ Vtx ⁡ ∅ = ∅