Definition df-rusgr

Description: Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read G RegUSGraph K as G is a K-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018) (Revised by AV, 18-Dec-2020)

	Ref	Expression
Assertion	df-rusgr	|- RegUSGraph = { <. g , k >. | ( g e. USGraph /\ g RegGraph k ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crusgr	|- RegUSGraph
1		vg	|- g
2		vk	|- k
3	1	cv	|- g
4		cusgr	|- USGraph
5	3 4	wcel	|- g e. USGraph
6		crgr	|- RegGraph
7	2	cv	|- k
8	3 7 6	wbr	|- g RegGraph k
9	5 8	wa	|- ( g e. USGraph /\ g RegGraph k )
10	9 1 2	copab	|- { <. g , k >. | ( g e. USGraph /\ g RegGraph k ) }
11	0 10	wceq	|- RegUSGraph = { <. g , k >. | ( g e. USGraph /\ g RegGraph k ) }