Metamath Proof Explorer

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 \in USGraph \land g RegGraph k)\}$

Detailed syntax breakdown

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