Definition df-rusgr 30018

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

Step	Hyp	Ref	Expression
1		crusgr 30016	. 2 class RegUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1569	. . . . 5 class 𝑔
4		cusgr 29609	. . . . 5 class USGraph
5	3, 4	wcel 2145	. . . 4 wff 𝑔 ∈ USGraph
6		vk	. . . . . 6 setvar 𝑘
7	6	cv 1569	. . . . 5 class 𝑘
8		crgr 30015	. . . . 5 class RegGraph
9	3, 7, 8	wbr 5103	. . . 4 wff 𝑔 RegGraph 𝑘
10	5, 9	wa 401	. . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
11	10, 2, 6	copab 5167	. 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
12	1, 11	wceq 1570	1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}

This definition is used by:  isrusgr  30021  rusgrprop  30022