Definition df-rusgr 27646

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 27644	. 2 class RegUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1542	. . . . 5 class 𝑔
4		cusgr 27240	. . . . 5 class USGraph
5	3, 4	wcel 2110	. . . 4 wff 𝑔 ∈ USGraph
6		vk	. . . . . 6 setvar 𝑘
7	6	cv 1542	. . . . 5 class 𝑘
8		crgr 27643	. . . . 5 class RegGraph
9	3, 7, 8	wbr 5053	. . . 4 wff 𝑔 RegGraph 𝑘
10	5, 9	wa 399	. . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
11	10, 2, 6	copab 5115	. 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
12	1, 11	wceq 1543	1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}

This definition is referenced by:  isrusgr  27649  rusgrprop  27650