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

Definition df-rgra 30665
Description: Define the set of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.)
Assertion
Ref Expression
df-rgra  |- RegGrph  =  { <. <. v ,  e
>. ,  k >.  |  ( k  e.  NN0  /\ 
A. p  e.  v  ( ( v VDeg  e
) `  p )  =  k ) }
Distinct variable group:    v, e, k, p

Detailed syntax breakdown of Definition df-rgra
StepHypRef Expression
1 crgra 30663 . 2  class RegGrph
2 vk . . . . . 6  setvar  k
32cv 1369 . . . . 5  class  k
4 cn0 10666 . . . . 5  class  NN0
53, 4wcel 1757 . . . 4  wff  k  e. 
NN0
6 vp . . . . . . . 8  setvar  p
76cv 1369 . . . . . . 7  class  p
8 vv . . . . . . . . 9  setvar  v
98cv 1369 . . . . . . . 8  class  v
10 ve . . . . . . . . 9  setvar  e
1110cv 1369 . . . . . . . 8  class  e
12 cvdg 23684 . . . . . . . 8  class VDeg
139, 11, 12co 6176 . . . . . . 7  class  ( v VDeg  e )
147, 13cfv 5502 . . . . . 6  class  ( ( v VDeg  e ) `  p )
1514, 3wceq 1370 . . . . 5  wff  ( ( v VDeg  e ) `  p )  =  k
1615, 6, 9wral 2792 . . . 4  wff  A. p  e.  v  ( (
v VDeg  e ) `  p )  =  k
175, 16wa 369 . . 3  wff  ( k  e.  NN0  /\  A. p  e.  v  ( (
v VDeg  e ) `  p )  =  k )
1817, 8, 10, 2coprab 6177 . 2  class  { <. <.
v ,  e >. ,  k >.  |  ( k  e.  NN0  /\  A. p  e.  v  ( ( v VDeg  e ) `
 p )  =  k ) }
191, 18wceq 1370 1  wff RegGrph  =  { <. <. v ,  e
>. ,  k >.  |  ( k  e.  NN0  /\ 
A. p  e.  v  ( ( v VDeg  e
) `  p )  =  k ) }
Colors of variables: wff setvar class
This definition is referenced by:  isrgra  30667  rgraprop  30669
  Copyright terms: Public domain W3C validator