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

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
StepHypRef Expression
1 cusg 25069 . 2  class USGrph
2 ve . . . . . 6  setvar  e
32cv 1447 . . . . 5  class  e
43cdm 4812 . . . 4  class  dom  e
5 vx . . . . . . . 8  setvar  x
65cv 1447 . . . . . . 7  class  x
7 chash 12509 . . . . . . 7  class  #
86, 7cfv 5561 . . . . . 6  class  ( # `  x )
9 c2 10648 . . . . . 6  class  2
108, 9wceq 1448 . . . . 5  wff  ( # `  x )  =  2
11 vv . . . . . . . 8  setvar  v
1211cv 1447 . . . . . . 7  class  v
1312cpw 3919 . . . . . 6  class  ~P v
14 c0 3699 . . . . . . 7  class  (/)
1514csn 3936 . . . . . 6  class  { (/) }
1613, 15cdif 3369 . . . . 5  class  ( ~P v  \  { (/) } )
1710, 5, 16crab 2741 . . . 4  class  { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x
)  =  2 }
184, 17, 3wf1 5558 . . 3  wff  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x
)  =  2 }
1918, 11, 2copab 4432 . 2  class  { <. v ,  e >.  |  e : dom  e -1-1-> {
x  e.  ( ~P v  \  { (/) } )  |  ( # `  x )  =  2 } }
201, 19wceq 1448 1  wff USGrph  =  { <. v ,  e >.  |  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/)
} )  |  (
# `  x )  =  2 } }
Colors of variables: wff setvar class
This definition is referenced by:  relusgra  25074  isusgra  25083  usgraop  25089
  Copyright terms: Public domain W3C validator