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

Definition df-rusgra 26452
 Description: Define the class of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.)
Assertion
Ref Expression
df-rusgra RegUSGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}
Distinct variable group:   𝑣,𝑒,𝑘

Detailed syntax breakdown of Definition df-rusgra
StepHypRef Expression
1 crusgra 26450 . 2 class RegUSGrph
2 vv . . . . . 6 setvar 𝑣
32cv 1474 . . . . 5 class 𝑣
4 ve . . . . . 6 setvar 𝑒
54cv 1474 . . . . 5 class 𝑒
6 cusg 25859 . . . . 5 class USGrph
73, 5, 6wbr 4583 . . . 4 wff 𝑣 USGrph 𝑒
83, 5cop 4131 . . . . 5 class 𝑣, 𝑒
9 vk . . . . . 6 setvar 𝑘
109cv 1474 . . . . 5 class 𝑘
11 crgra 26449 . . . . 5 class RegGrph
128, 10, 11wbr 4583 . . . 4 wff 𝑣, 𝑒⟩ RegGrph 𝑘
137, 12wa 383 . . 3 wff (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)
1413, 2, 4, 9coprab 6550 . 2 class {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}
151, 14wceq 1475 1 wff RegUSGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}
 Colors of variables: wff setvar class This definition is referenced by:  isrusgra  26454  rusgraprop  26456  rusgrargra  26457
 Copyright terms: Public domain W3C validator