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 VDeg
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-rgra
StepHypRef Expression
1 crgra 25646 . 2 RegGrph
2 vk . . . . . 6
32cv 1437 . . . . 5
4 cn0 10875 . . . . 5
53, 4wcel 1869 . . . 4
6 vp . . . . . . . 8
76cv 1437 . . . . . . 7
8 vv . . . . . . . . 9
98cv 1437 . . . . . . . 8
10 ve . . . . . . . . 9
1110cv 1437 . . . . . . . 8
12 cvdg 25617 . . . . . . . 8 VDeg
139, 11, 12co 6304 . . . . . . 7 VDeg
147, 13cfv 5600 . . . . . 6 VDeg
1514, 3wceq 1438 . . . . 5 VDeg
1615, 6, 9wral 2776 . . . 4 VDeg
175, 16wa 371 . . 3 VDeg
1817, 8, 10, 2coprab 6305 . 2 VDeg
191, 18wceq 1438 1 RegGrph VDeg
 Colors of variables: wff setvar class This definition is referenced by:  isrgra  25650  rgraprop  25652
 Copyright terms: Public domain W3C validator