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 ‘ ∅ ) = ∅