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

Step	Hyp	Ref	Expression
1		crusgr 40756	. 2 class RegUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1474	. . . . 5 class 𝑔
4		cusgr 40379	. . . . 5 class USGraph
5	3, 4	wcel 1977	. . . 4 wff 𝑔 ∈ USGraph
6		vk	. . . . . 6 setvar 𝑘
7	6	cv 1474	. . . . 5 class 𝑘
8		crgr 40755	. . . . 5 class RegGraph
9	3, 7, 8	wbr 4583	. . . 4 wff 𝑔 RegGraph 𝑘
10	5, 9	wa 383	. . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
11	10, 2, 6	copab 4642	. 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
12	1, 11	wceq 1475	1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}

This definition is referenced by:  isrusgr  40761  rusgrprop  40762