Theorem isrusgr

Description: The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018) (Revised by AV, 18-Dec-2020)

	Ref	Expression
Assertion	isrusgr	|- ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ G RegGraph K ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( g = G -> ( g e. USGraph <-> G e. USGraph ) )
2	1	adantr	|- ( ( g = G /\ k = K ) -> ( g e. USGraph <-> G e. USGraph ) )
3		breq12	|- ( ( g = G /\ k = K ) -> ( g RegGraph k <-> G RegGraph K ) )
4	2 3	anbi12d	|- ( ( g = G /\ k = K ) -> ( ( g e. USGraph /\ g RegGraph k ) <-> ( G e. USGraph /\ G RegGraph K ) ) )
5		df-rusgr	|- RegUSGraph = { <. g , k >. | ( g e. USGraph /\ g RegGraph k ) }
6	4 5	brabga	|- ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ G RegGraph K ) ) )