Metamath Proof Explorer


Definition df-rusgr

Description: Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read G RegUSGraph K as G is a K-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 18-Dec-2020)

Ref Expression
Assertion df-rusgr RegUSGraph = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crusgr RegUSGraph
1 vg 𝑔
2 vk 𝑘
3 1 cv 𝑔
4 cusgr USGraph
5 3 4 wcel 𝑔 ∈ USGraph
6 crgr RegGraph
7 2 cv 𝑘
8 3 7 6 wbr 𝑔 RegGraph 𝑘
9 5 8 wa ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 )
10 9 1 2 copab { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }
11 0 10 wceq RegUSGraph = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }