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 
 |-  -. (/) e. ( _V X. _V )
2 1 iffalsei 
 |-  if ( (/) e. ( _V X. _V ) , ( 1st ` (/) ) , ( Base ` (/) ) ) = ( Base ` (/) )
3 vtxval 
 |-  ( Vtx ` (/) ) = if ( (/) e. ( _V X. _V ) , ( 1st ` (/) ) , ( Base ` (/) ) )
4 base0 
 |-  (/) = ( Base ` (/) )
5 2 3 4 3eqtr4i 
 |-  ( Vtx ` (/) ) = (/)