Definition df-usgra 24538

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 24535	. 2 class USGrph
2		ve	. . . . . 6 setvar e
3	2	cv 1397	. . . . 5 class e
4	3	cdm 4988	. . . 4 class dom e
5		vx	. . . . . . . 8 setvar x
6	5	cv 1397	. . . . . . 7 class x
7		chash 12390	. . . . . . 7 class #
8	6, 7	cfv 5570	. . . . . 6 class ( # ` x )
9		c2 10581	. . . . . 6 class 2
10	8, 9	wceq 1398	. . . . 5 wff ( # ` x ) = 2
11		vv	. . . . . . . 8 setvar v
12	11	cv 1397	. . . . . . 7 class v
13	12	cpw 3999	. . . . . 6 class ~P v
14		c0 3783	. . . . . . 7 class (/)
15	14	csn 4016	. . . . . 6 class { (/) }
16	13, 15	cdif 3458	. . . . 5 class ( ~P v \ { (/) } )
17	10, 5, 16	crab 2808	. . . 4 class { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
18	4, 17, 3	wf1 5567	. . 3 wff e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
19	18, 11, 2	copab 4496	. 2 class { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }
20	1, 19	wceq 1398	1 wff USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }

This definition is referenced by:  relusgra  24540  isusgra  24549  usgraop  24555