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 = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crusgr	⊢ RegUSGraph
1		vg	⊢ 𝑔
2		vk	⊢ 𝑘
3	1	cv	⊢ 𝑔
4		cusgr	⊢ USGraph
5	3 4	wcel	⊢ 𝑔 ∈ USGraph
6		crgr	⊢ RegGraph
7	2	cv	⊢ 𝑘
8	3 7 6	wbr	⊢ 𝑔 RegGraph 𝑘
9	5 8	wa	⊢ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 )
10	9 1 2	copab	⊢ { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }
11	0 10	wceq	⊢ RegUSGraph = { ⟨ 𝑔 , 𝑘 ⟩ ∣ ( 𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘 ) }