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

Definition df-rgra 26451
 Description: Define the class of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.)
Assertion
Ref Expression
df-rgra RegGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}
Distinct variable group:   𝑣,𝑒,𝑘,𝑝

Detailed syntax breakdown of Definition df-rgra
StepHypRef Expression
1 crgra 26449 . 2 class RegGrph
2 vk . . . . . 6 setvar 𝑘
32cv 1474 . . . . 5 class 𝑘
4 cn0 11169 . . . . 5 class 0
53, 4wcel 1977 . . . 4 wff 𝑘 ∈ ℕ0
6 vp . . . . . . . 8 setvar 𝑝
76cv 1474 . . . . . . 7 class 𝑝
8 vv . . . . . . . . 9 setvar 𝑣
98cv 1474 . . . . . . . 8 class 𝑣
10 ve . . . . . . . . 9 setvar 𝑒
1110cv 1474 . . . . . . . 8 class 𝑒
12 cvdg 26420 . . . . . . . 8 class VDeg
139, 11, 12co 6549 . . . . . . 7 class (𝑣 VDeg 𝑒)
147, 13cfv 5804 . . . . . 6 class ((𝑣 VDeg 𝑒)‘𝑝)
1514, 3wceq 1475 . . . . 5 wff ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘
1615, 6, 9wral 2896 . . . 4 wff 𝑝𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘
175, 16wa 383 . . 3 wff (𝑘 ∈ ℕ0 ∧ ∀𝑝𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)
1817, 8, 10, 2coprab 6550 . 2 class {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}
191, 18wceq 1475 1 wff RegGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}
 Colors of variables: wff setvar class This definition is referenced by:  isrgra  26453  rgraprop  26455
 Copyright terms: Public domain W3C validator