Definition df-edg 25111

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 for any ordered pairs as the range of its second component (which even needs not to be a function). Therefore, this definition could also be used for hypergraphs and multigraphs. In these cases, however, the (possibly more than one) edges connecting the same vertices could not be distinguished anymore. Therefore, this definition should only be used for undirected simple graphs. (Contributed by AV, 1-Jan-2020.)

Assertion

Ref	Expression
df-edg	|- Edges = ( g e. _V |-> ran ( 2nd ` g ) )

Detailed syntax breakdown of Definition df-edg

Step	Hyp	Ref	Expression
1		cedg 25106	. 2 class Edges
2		vg	. . 3 setvar g
3		cvv 3056	. . 3 class _V
4	2	cv 1453	. . . . 5 class g
5		c2nd 6818	. . . . 5 class 2nd
6	4, 5	cfv 5600	. . . 4 class ( 2nd ` g )
7	6	crn 4853	. . 3 class ran ( 2nd ` g )
8	2, 3, 7	cmpt 4474	. 2 class ( g e. _V |-> ran ( 2nd ` g ) )
9	1, 8	wceq 1454	1 wff Edges = ( g e. _V |-> ran ( 2nd ` g ) )

This definition is referenced by:  edgval  25114