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	$$⊢\mathrm{iEdg}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0nelxp	$$⊢\neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
2	1	iffalsei	$$⊢if\left(\varnothing \in \left(\mathrm{V}\times \mathrm{V}\right),2^{nd}\left(\varnothing \right),\mathrm{ef}\left(\varnothing \right)\right)=\mathrm{ef}\left(\varnothing \right)$$
3		iedgval	$$⊢\mathrm{iEdg}\left(\varnothing \right)=if\left(\varnothing \in \left(\mathrm{V}\times \mathrm{V}\right),2^{nd}\left(\varnothing \right),\mathrm{ef}\left(\varnothing \right)\right)$$
4		df-edgf	$$⊢\mathrm{ef}=\mathrm{Slot}18$$
5	4	str0	$$⊢\varnothing =\mathrm{ef}\left(\varnothing \right)$$
6	2 3 5	3eqtr4i	$$⊢\mathrm{iEdg}\left(\varnothing \right)=\varnothing$$