Definition df-rusgr 28812

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 28810	. 2 class RegUSGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1540	. . . . 5 class 𝑔
4		cusgr 28406	. . . . 5 class USGraph
5	3, 4	wcel 2106	. . . 4 wff 𝑔 ∈ USGraph
6		vk	. . . . . 6 setvar 𝑘
7	6	cv 1540	. . . . 5 class 𝑘
8		crgr 28809	. . . . 5 class RegGraph
9	3, 7, 8	wbr 5148	. . . 4 wff 𝑔 RegGraph 𝑘
10	5, 9	wa 396	. . 3 wff (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)
11	10, 2, 6	copab 5210	. 2 class {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
12	1, 11	wceq 1541	1 wff RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}

This definition is referenced by:  isrusgr  28815  rusgrprop  28816