Definition df-usgra 25072

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 25069	. 2 class USGrph
2		ve	. . . . . 6 setvar e
3	2	cv 1447	. . . . 5 class e
4	3	cdm 4812	. . . 4 class dom e
5		vx	. . . . . . . 8 setvar x
6	5	cv 1447	. . . . . . 7 class x
7		chash 12509	. . . . . . 7 class #
8	6, 7	cfv 5561	. . . . . 6 class ( # ` x )
9		c2 10648	. . . . . 6 class 2
10	8, 9	wceq 1448	. . . . 5 wff ( # ` x ) = 2
11		vv	. . . . . . . 8 setvar v
12	11	cv 1447	. . . . . . 7 class v
13	12	cpw 3919	. . . . . 6 class ~P v
14		c0 3699	. . . . . . 7 class (/)
15	14	csn 3936	. . . . . 6 class { (/) }
16	13, 15	cdif 3369	. . . . 5 class ( ~P v \ { (/) } )
17	10, 5, 16	crab 2741	. . . 4 class { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
18	4, 17, 3	wf1 5558	. . 3 wff e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
19	18, 11, 2	copab 4432	. 2 class { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }
20	1, 19	wceq 1448	1 wff USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }

This definition is referenced by:  relusgra  25074  isusgra  25083  usgraop  25089