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

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
StepHypRef Expression
1 cusg 21318 . 2  class USGrph
2 ve . . . . . 6  set  e
32cv 1648 . . . . 5  class  e
43cdm 4837 . . . 4  class  dom  e
5 vx . . . . . . . 8  set  x
65cv 1648 . . . . . . 7  class  x
7 chash 11573 . . . . . . 7  class  #
86, 7cfv 5413 . . . . . 6  class  ( # `  x )
9 c2 10005 . . . . . 6  class  2
108, 9wceq 1649 . . . . 5  wff  ( # `  x )  =  2
11 vv . . . . . . . 8  set  v
1211cv 1648 . . . . . . 7  class  v
1312cpw 3759 . . . . . 6  class  ~P v
14 c0 3588 . . . . . . 7  class  (/)
1514csn 3774 . . . . . 6  class  { (/) }
1613, 15cdif 3277 . . . . 5  class  ( ~P v  \  { (/) } )
1710, 5, 16crab 2670 . . . 4  class  { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x
)  =  2 }
184, 17, 3wf1 5410 . . 3  wff  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x
)  =  2 }
1918, 11, 2copab 4225 . 2  class  { <. v ,  e >.  |  e : dom  e -1-1-> {
x  e.  ( ~P v  \  { (/) } )  |  ( # `  x )  =  2 } }
201, 19wceq 1649 1  wff USGrph  =  { <. v ,  e >.  |  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/)
} )  |  (
# `  x )  =  2 } }
Colors of variables: wff set class
This definition is referenced by:  relusgra  21322  isusgra  21326
  Copyright terms: Public domain W3C validator