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 ) , ( 1st ‘ ∅ ) , ( Base ‘ ∅ ) ) = ( Base ‘ ∅ )
3 vtxval ( Vtx ‘ ∅ ) = if ( ∅ ∈ ( V × V ) , ( 1st ‘ ∅ ) , ( Base ‘ ∅ ) )
4 base0 ∅ = ( Base ‘ ∅ )
5 2 3 4 3eqtr4i ( Vtx ‘ ∅ ) = ∅