Definition df-rusgra 26452

Description: Define the class of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.)

Assertion

Ref	Expression
df-rusgra	⊢ RegUSGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}

Distinct variable group:   𝑣,𝑒,𝑘

Detailed syntax breakdown of Definition df-rusgra

Step	Hyp	Ref	Expression
1		crusgra 26450	. 2 class RegUSGrph
2		vv	. . . . . 6 setvar 𝑣
3	2	cv 1474	. . . . 5 class 𝑣
4		ve	. . . . . 6 setvar 𝑒
5	4	cv 1474	. . . . 5 class 𝑒
6		cusg 25859	. . . . 5 class USGrph
7	3, 5, 6	wbr 4583	. . . 4 wff 𝑣 USGrph 𝑒
8	3, 5	cop 4131	. . . . 5 class ⟨𝑣, 𝑒⟩
9		vk	. . . . . 6 setvar 𝑘
10	9	cv 1474	. . . . 5 class 𝑘
11		crgra 26449	. . . . 5 class RegGrph
12	8, 10, 11	wbr 4583	. . . 4 wff ⟨𝑣, 𝑒⟩ RegGrph 𝑘
13	7, 12	wa 383	. . 3 wff (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)
14	13, 2, 4, 9	coprab 6550	. 2 class {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}
15	1, 14	wceq 1475	1 wff RegUSGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑣 USGrph 𝑒 ∧ ⟨𝑣, 𝑒⟩ RegGrph 𝑘)}

This definition is referenced by:  isrusgra  26454  rusgraprop  26456  rusgrargra  26457