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

Definition df-rgra 25648
Description: Define the class 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 25646 . 2  class RegGrph
2 vk . . . . . 6  setvar  k
32cv 1437 . . . . 5  class  k
4 cn0 10875 . . . . 5  class  NN0
53, 4wcel 1869 . . . 4  wff  k  e. 
NN0
6 vp . . . . . . . 8  setvar  p
76cv 1437 . . . . . . 7  class  p
8 vv . . . . . . . . 9  setvar  v
98cv 1437 . . . . . . . 8  class  v
10 ve . . . . . . . . 9  setvar  e
1110cv 1437 . . . . . . . 8  class  e
12 cvdg 25617 . . . . . . . 8  class VDeg
139, 11, 12co 6304 . . . . . . 7  class  ( v VDeg  e )
147, 13cfv 5600 . . . . . 6  class  ( ( v VDeg  e ) `  p )
1514, 3wceq 1438 . . . . 5  wff  ( ( v VDeg  e ) `  p )  =  k
1615, 6, 9wral 2776 . . . 4  wff  A. p  e.  v  ( (
v VDeg  e ) `  p )  =  k
175, 16wa 371 . . 3  wff  ( k  e.  NN0  /\  A. p  e.  v  ( (
v VDeg  e ) `  p )  =  k )
1817, 8, 10, 2coprab 6305 . 2  class  { <. <.
v ,  e >. ,  k >.  |  ( k  e.  NN0  /\  A. p  e.  v  ( ( v VDeg  e ) `
 p )  =  k ) }
191, 18wceq 1438 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  25650  rgraprop  25652
  Copyright terms: Public domain W3C validator