Metamath Proof Explorer

Theorem rusgrprop

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

Ref Expression
Assertion rusgrprop ⊢ G RegUSGraph K → G ∈ USGraph ∧ G RegGraph K

Proof

Step Hyp Ref Expression
1 df-rusgr ⊢ RegUSGraph = g k | g ∈ USGraph ∧ g RegGraph k
2 1 bropaex12 ⊢ G RegUSGraph K → G ∈ V ∧ K ∈ V
3 isrusgr ⊢ G ∈ V ∧ K ∈ V → G RegUSGraph K ↔ G ∈ USGraph ∧ G RegGraph K
4 3 biimpd ⊢ G ∈ V ∧ K ∈ V → G RegUSGraph K → G ∈ USGraph ∧ G RegGraph K
5 2 4 mpcom ⊢ G RegUSGraph K → G ∈ USGraph ∧ G RegGraph K