Definition df-usgra 21320

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 itsself). (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 21318	. 2 class USGrph
2		ve	. . . . . 6 set e
3	2	cv 1648	. . . . 5 class e
4	3	cdm 4837	. . . 4 class dom e
5		vx	. . . . . . . 8 set x
6	5	cv 1648	. . . . . . 7 class x
7		chash 11573	. . . . . . 7 class #
8	6, 7	cfv 5413	. . . . . 6 class ( # ` x )
9		c2 10005	. . . . . 6 class 2
10	8, 9	wceq 1649	. . . . 5 wff ( # ` x ) = 2
11		vv	. . . . . . . 8 set v
12	11	cv 1648	. . . . . . 7 class v
13	12	cpw 3759	. . . . . 6 class ~P v
14		c0 3588	. . . . . . 7 class (/)
15	14	csn 3774	. . . . . 6 class { (/) }
16	13, 15	cdif 3277	. . . . 5 class ( ~P v \ { (/) } )
17	10, 5, 16	crab 2670	. . . 4 class { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
18	4, 17, 3	wf1 5410	. . 3 wff e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 }
19	18, 11, 2	copab 4225	. 2 class { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }
20	1, 19	wceq 1649	1 wff USGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) = 2 } }

This definition is referenced by:  relusgra  21322  isusgra  21326