Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rusgra Structured version   Unicode version

Definition df-rusgra 30682
Description: Define the set of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.)
Assertion
Ref Expression
df-rusgra  |- RegUSGrph  =  { <. <. v ,  e
>. ,  k >.  |  ( v USGrph  e  /\  <.
v ,  e >. RegGrph  k ) }
Distinct variable group:    v, e, k

Detailed syntax breakdown of Definition df-rusgra
StepHypRef Expression
1 crusgra 30680 . 2  class RegUSGrph
2 vv . . . . . 6  setvar  v
32cv 1369 . . . . 5  class  v
4 ve . . . . . 6  setvar  e
54cv 1369 . . . . 5  class  e
6 cusg 23401 . . . . 5  class USGrph
73, 5, 6wbr 4392 . . . 4  wff  v USGrph  e
83, 5cop 3983 . . . . 5  class  <. v ,  e >.
9 vk . . . . . 6  setvar  k
109cv 1369 . . . . 5  class  k
11 crgra 30679 . . . . 5  class RegGrph
128, 10, 11wbr 4392 . . . 4  wff  <. v ,  e >. RegGrph  k
137, 12wa 369 . . 3  wff  ( v USGrph 
e  /\  <. v ,  e >. RegGrph  k )
1413, 2, 4, 9coprab 6193 . 2  class  { <. <.
v ,  e >. ,  k >.  |  ( v USGrph  e  /\  <. v ,  e >. RegGrph  k ) }
151, 14wceq 1370 1  wff RegUSGrph  =  { <. <. v ,  e
>. ,  k >.  |  ( v USGrph  e  /\  <.
v ,  e >. RegGrph  k ) }
Colors of variables: wff setvar class
This definition is referenced by:  isrusgra  30684  rusgraprop  30686  rusgrargra  30687
  Copyright terms: Public domain W3C validator