Metamath Proof Explorer

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 ∈ W ∧ K ∈ Z → G RegUSGraph K ↔ G ∈ USGraph ∧ G RegGraph K

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ g = G → g ∈ USGraph ↔ G ∈ USGraph
2 1 adantr ⊢ g = G ∧ k = K → g ∈ USGraph ↔ G ∈ USGraph
3 breq12 ⊢ g = G ∧ k = K → g RegGraph k ↔ G RegGraph K
4 2 3 anbi12d ⊢ g = G ∧ k = K → g ∈ USGraph ∧ g RegGraph k ↔ G ∈ USGraph ∧ G RegGraph K
5 df-rusgr ⊢ RegUSGraph = g k | g ∈ USGraph ∧ g RegGraph k
6 4 5 brabga ⊢ G ∈ W ∧ K ∈ Z → G RegUSGraph K ↔ G ∈ USGraph ∧ G RegGraph K