Definition df-usgra 24037

Description: Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph <. V , E >. where E is an injective (one-to-one) function into subsets of V of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itself). (Contributed by Alexander van der Vekens, 10-Aug-2017.)

Assertion

Ref	Expression
df-usgra	|- USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }

Distinct variable group:   v, e, x

Detailed syntax breakdown of Definition df-usgra

Step	Hyp	Ref	Expression
1		cusg 24034	. 2 class USGrph
2		ve	. . . . . 6 setvar e
3	2	cv 1378	. . . . 5 class e
4	3	cdm 4999	. . . 4 class dom e
5		vx	. . . . . . . 8 setvar x
6	5	cv 1378	. . . . . . 7 class x
7		chash 12373	. . . . . . 7 class #
8	6, 7	cfv 5588	. . . . . 6 class ( # ` x )
9		c2 10585	. . . . . 6 class 2
10	8, 9	wceq 1379	. . . . 5 wff ( # ` x ) = 2
11		vv	. . . . . . . 8 setvar v
12	11	cv 1378	. . . . . . 7 class v
13	12	cpw 4010	. . . . . 6 class ~P v
14		c0 3785	. . . . . . 7 class (/)
15	14	csn 4027	. . . . . 6 class { (/) }
16	13, 15	cdif 3473	. . . . 5 class ( ~P v \ { (/) } )
17	10, 5, 16	crab 2818	. . . 4 class { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
18	4, 17, 3	wf1 5585	. . 3 wff e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
19	18, 11, 2	copab 4504	. 2 class { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }
20	1, 19	wceq 1379	1 wff USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }

This definition is referenced by:  relusgra  24039  isusgra  24048  usgraop  24054