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 26664
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 26662 . 2 class RegUSGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1631 . . . . 5 class 𝑔
4 cusgr 26243 . . . . 5 class USGraph
53, 4wcel 2139 . . . 4 wff 𝑔 ∈ USGraph
6 vk . . . . . 6 setvar 𝑘
76cv 1631 . . . . 5 class 𝑘
8 crgr 26661 . . . . 5 class RegGraph
93, 7, 8wbr 4804 . . . 4 wff 𝑔RegGraph𝑘
105, 9wa 383 . . 3 wff (𝑔 ∈ USGraph ∧ 𝑔RegGraph𝑘)
1110, 2, 6copab 4864 . 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔RegGraph𝑘)}
121, 11wceq 1632 1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔RegGraph𝑘)}
Colors of variables: wff setvar class
This definition is referenced by:  isrusgr  26667  rusgrprop  26668
  Copyright terms: Public domain W3C validator