Definition df-rgra 26451

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

Assertion

Ref	Expression
df-rgra	⊢ RegGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}

Distinct variable group:   𝑣,𝑒,𝑘,𝑝

Detailed syntax breakdown of Definition df-rgra

Step	Hyp	Ref	Expression
1		crgra 26449	. 2 class RegGrph
2		vk	. . . . . 6 setvar 𝑘
3	2	cv 1474	. . . . 5 class 𝑘
4		cn0 11169	. . . . 5 class ℕ0
5	3, 4	wcel 1977	. . . 4 wff 𝑘 ∈ ℕ0
6		vp	. . . . . . . 8 setvar 𝑝
7	6	cv 1474	. . . . . . 7 class 𝑝
8		vv	. . . . . . . . 9 setvar 𝑣
9	8	cv 1474	. . . . . . . 8 class 𝑣
10		ve	. . . . . . . . 9 setvar 𝑒
11	10	cv 1474	. . . . . . . 8 class 𝑒
12		cvdg 26420	. . . . . . . 8 class VDeg
13	9, 11, 12	co 6549	. . . . . . 7 class (𝑣 VDeg 𝑒)
14	7, 13	cfv 5804	. . . . . 6 class ((𝑣 VDeg 𝑒)‘𝑝)
15	14, 3	wceq 1475	. . . . 5 wff ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘
16	15, 6, 9	wral 2896	. . . 4 wff ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘
17	5, 16	wa 383	. . 3 wff (𝑘 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)
18	17, 8, 10, 2	coprab 6550	. 2 class {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}
19	1, 18	wceq 1475	1 wff RegGrph = {⟨⟨𝑣, 𝑒⟩, 𝑘⟩ ∣ (𝑘 ∈ ℕ0 ∧ ∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}

This definition is referenced by:  isrgra  26453  rgraprop  26455