Metamath Proof Explorer


Definition df-edg

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 (e.g., edguhgr ). 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)

Ref Expression
Assertion df-edg Edg = g V ran iEdg g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cedg class Edg
1 vg setvar g
2 cvv class V
3 ciedg class iEdg
4 1 cv setvar g
5 4 3 cfv class iEdg g
6 5 crn class ran iEdg g
7 1 2 6 cmpt class g V ran iEdg g
8 0 7 wceq wff Edg = g V ran iEdg g