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

Definition df-rusgr 27267
Description: Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read 𝐺 RegUSGraph 𝐾 as 𝐺 is a 𝐾-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.)
Assertion
Ref Expression
df-rusgr RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
Distinct variable group:   𝑔,𝑘

Detailed syntax breakdown of Definition df-rusgr
StepHypRef Expression
1 crusgr 27265 . 2 class RegUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1527 . . . . 5 class 𝑔
4 cusgr 26861 . . . . 5 class USGraph
53, 4wcel 2105 . . . 4 wff 𝑔 ∈ USGraph
6 vk . . . . . 6 setvar 𝑘
76cv 1527 . . . . 5 class 𝑘
8 crgr 27264 . . . . 5 class RegGraph
93, 7, 8wbr 5057 . . . 4 wff 𝑔 RegGraph 𝑘
105, 9wa 396 . . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
1110, 2, 6copab 5119 . 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
121, 11wceq 1528 1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
Colors of variables: wff setvar class
This definition is referenced by:  isrusgr  27270  rusgrprop  27271
  Copyright terms: Public domain W3C validator