Metamath Proof Explorer

Theorem iedgval0

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

Ref Expression
Assertion iedgval0 
|- ( iEdg ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 0nelxp 
 |-  -. (/) e. ( _V X. _V )
2 1 iffalsei 
 |-  if ( (/) e. ( _V X. _V ) , ( 2nd ` (/) ) , ( .ef ` (/) ) ) = ( .ef ` (/) )
3 iedgval 
 |-  ( iEdg ` (/) ) = if ( (/) e. ( _V X. _V ) , ( 2nd ` (/) ) , ( .ef ` (/) ) )
4 edgfid 
 |-  .ef = Slot ( .ef ` ndx )
5 4 str0 
 |-  (/) = ( .ef ` (/) )
6 2 3 5 3eqtr4i 
 |-  ( iEdg ` (/) ) = (/)