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

Definition df-rusgr 27355
 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 27353 . 2 class RegUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1537 . . . . 5 class 𝑔
4 cusgr 26949 . . . . 5 class USGraph
53, 4wcel 2111 . . . 4 wff 𝑔 ∈ USGraph
6 vk . . . . . 6 setvar 𝑘
76cv 1537 . . . . 5 class 𝑘
8 crgr 27352 . . . . 5 class RegGraph
93, 7, 8wbr 5030 . . . 4 wff 𝑔 RegGraph 𝑘
105, 9wa 399 . . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
1110, 2, 6copab 5092 . 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
121, 11wceq 1538 1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
 Colors of variables: wff setvar class This definition is referenced by:  isrusgr  27358  rusgrprop  27359
 Copyright terms: Public domain W3C validator