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 =