Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rusgr Structured version   Visualization version   GIF version

Definition df-rusgr 40758
 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 40756 . 2 class RegUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1474 . . . . 5 class 𝑔
4 cusgr 40379 . . . . 5 class USGraph
53, 4wcel 1977 . . . 4 wff 𝑔 ∈ USGraph
6 vk . . . . . 6 setvar 𝑘
76cv 1474 . . . . 5 class 𝑘
8 crgr 40755 . . . . 5 class RegGraph
93, 7, 8wbr 4583 . . . 4 wff 𝑔 RegGraph 𝑘
105, 9wa 383 . . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
1110, 2, 6copab 4642 . 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
121, 11wceq 1475 1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
 Colors of variables: wff setvar class This definition is referenced by:  isrusgr  40761  rusgrprop  40762
 Copyright terms: Public domain W3C validator