Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-usgra Structured version   Unicode version

Definition df-usgra 21367
 Description: Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph where is an injective (one-to-one) function into subsets of 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-usgra
StepHypRef Expression
1 cusg 21365 . 2 USGrph
2 ve . . . . . 6
32cv 1651 . . . . 5
43cdm 4878 . . . 4
5 vx . . . . . . . 8
65cv 1651 . . . . . . 7
7 chash 11618 . . . . . . 7
86, 7cfv 5454 . . . . . 6
9 c2 10049 . . . . . 6
108, 9wceq 1652 . . . . 5
11 vv . . . . . . . 8
1211cv 1651 . . . . . . 7
1312cpw 3799 . . . . . 6
14 c0 3628 . . . . . . 7
1514csn 3814 . . . . . 6
1613, 15cdif 3317 . . . . 5
1710, 5, 16crab 2709 . . . 4
184, 17, 3wf1 5451 . . 3
1918, 11, 2copab 4265 . 2
201, 19wceq 1652 1 USGrph
 Colors of variables: wff set class This definition is referenced by:  relusgra  21369  isusgra  21373
 Copyright terms: Public domain W3C validator