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	$$⊢\mathrm{RegUSGraph}=\left\{⟨g,k⟩|\left(g\in \mathrm{USGraph}\wedge g\mathrm{RegGraph}k\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crusgr	$$class\mathrm{RegUSGraph}$$
1		vg	$$setvarg$$
2		vk	$$setvark$$
3	1	cv	$$setvarg$$
4		cusgr	$$class\mathrm{USGraph}$$
5	3 4	wcel	$$wffg\in \mathrm{USGraph}$$
6		crgr	$$class\mathrm{RegGraph}$$
7	2	cv	$$setvark$$
8	3 7 6	wbr	$$wffg\mathrm{RegGraph}k$$
9	5 8	wa	$$wff\left(g\in \mathrm{USGraph}\wedge g\mathrm{RegGraph}k\right)$$
10	9 1 2	copab	$$class\left\{⟨g,k⟩|\left(g\in \mathrm{USGraph}\wedge g\mathrm{RegGraph}k\right)\right\}$$
11	0 10	wceq	$$wff\mathrm{RegUSGraph}=\left\{⟨g,k⟩|\left(g\in \mathrm{USGraph}\wedge g\mathrm{RegGraph}k\right)\right\}$$