Definition df-edg 15982

Description: Define the class of edges of a graph, see also definition "E = E(G)" in section I.1 of [Bollobas] p. 1. This definition is very general: It defines edges of a class as the range of its edge function (which does not even need to be a function). Therefore, this definition could also be used for hypergraphs, pseudographs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. In some cases, this is no problem, so theorems with Edg are meaningful nevertheless. Usually, however, this definition is used only for undirected simple (hyper-/pseudo-)graphs (with or without loops). (Contributed by AV, 1-Jan-2020.) (Revised by AV, 13-Oct-2020.)

Assertion

Ref	Expression
df-edg	⊢ Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))

Detailed syntax breakdown of Definition df-edg

Step	Hyp	Ref	Expression
1		cedg 15981	. 2 class Edg
2		vg	. . 3 setvar 𝑔
3		cvv 2803	. . 3 class V
4	2	cv 1397	. . . . 5 class 𝑔
5		ciedg 15937	. . . . 5 class iEdg
6	4, 5	cfv 5333	. . . 4 class (iEdg‘𝑔)
7	6	crn 4732	. . 3 class ran (iEdg‘𝑔)
8	2, 3, 7	cmpt 4155	. 2 class (𝑔 ∈ V ↦ ran (iEdg‘𝑔))
9	1, 8	wceq 1398	1 wff Edg = (𝑔 ∈ V ↦ ran (iEdg‘𝑔))

This definition is referenced by:  edgvalg  15983  edgval  15984  edgopval  15986  edgstruct  15988