Definition df-rgr 26453

Description: Define the "k-regular" predicate, which is true for a "graph" being k-regular: read G RegGraph K as " G is K-regular" or " G is a K-regular graph". Note that K is allowed to be positive infinity ( K e. NN0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.)

Assertion

Ref	Expression
df-rgr	|- RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. (Vtx ` g ) ( (VtxDeg ` g ) ` v ) = k ) }

Distinct variable group:   g, k, v

Detailed syntax breakdown of Definition df-rgr

Step	Hyp	Ref	Expression
1		crgr 26451	. 2 class RegGraph
2		vk	. . . . . 6 setvar k
3	2	cv 1482	. . . . 5 class k
4		cxnn0 11363	. . . . 5 class NN0*
5	3, 4	wcel 1990	. . . 4 wff k e. NN0*
6		vv	. . . . . . . 8 setvar v
7	6	cv 1482	. . . . . . 7 class v
8		vg	. . . . . . . . 9 setvar g
9	8	cv 1482	. . . . . . . 8 class g
10		cvtxdg 26361	. . . . . . . 8 class VtxDeg
11	9, 10	cfv 5888	. . . . . . 7 class (VtxDeg ` g )
12	7, 11	cfv 5888	. . . . . 6 class ( (VtxDeg ` g ) ` v )
13	12, 3	wceq 1483	. . . . 5 wff ( (VtxDeg ` g ) ` v ) = k
14		cvtx 25874	. . . . . 6 class Vtx
15	9, 14	cfv 5888	. . . . 5 class (Vtx ` g )
16	13, 6, 15	wral 2912	. . . 4 wff A. v e. (Vtx ` g ) ( (VtxDeg ` g ) ` v ) = k
17	5, 16	wa 384	. . 3 wff ( k e. NN0* /\ A. v e. (Vtx ` g ) ( (VtxDeg ` g ) ` v ) = k )
18	17, 8, 2	copab 4712	. 2 class { <. g , k >. | ( k e. NN0* /\ A. v e. (Vtx ` g ) ( (VtxDeg ` g ) ` v ) = k ) }
19	1, 18	wceq 1483	1 wff RegGraph = { <. g , k >. | ( k e. NN0* /\ A. v e. (Vtx ` g ) ( (VtxDeg ` g ) ` v ) = k ) }

This definition is referenced by:  isrgr  26455  rgrprop  26456