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

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