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 ¬ ∅ ∈ ( V × V )
2 1 iffalsei if ( ∅ ∈ ( V × V ) , ( 2nd ‘ ∅ ) , ( .ef ‘ ∅ ) ) = ( .ef ‘ ∅ )
3 iedgval ( iEdg ‘ ∅ ) = if ( ∅ ∈ ( V × V ) , ( 2nd ‘ ∅ ) , ( .ef ‘ ∅ ) )
4 edgfid .ef = Slot ( .ef ‘ ndx )
5 4 str0 ∅ = ( .ef ‘ ∅ )
6 2 3 5 3eqtr4i ( iEdg ‘ ∅ ) = ∅