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		df-edgf	⊢ .ef = Slot ; 1 8
5	4	str0	⊢ ∅ = ( .ef ‘ ∅ )
6	2 3 5	3eqtr4i	⊢ ( iEdg ‘ ∅ ) = ∅