Step |
Hyp |
Ref |
Expression |
1 |
|
isrusgr0.v |
|- V = ( Vtx ` G ) |
2 |
|
isrusgr0.d |
|- D = ( VtxDeg ` G ) |
3 |
|
isrusgr |
|- ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ G RegGraph K ) ) ) |
4 |
1 2
|
isrgr |
|- ( ( G e. W /\ K e. Z ) -> ( G RegGraph K <-> ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |
5 |
4
|
anbi2d |
|- ( ( G e. W /\ K e. Z ) -> ( ( G e. USGraph /\ G RegGraph K ) <-> ( G e. USGraph /\ ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) ) |
6 |
|
3anass |
|- ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) <-> ( G e. USGraph /\ ( K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |
7 |
5 6
|
bitr4di |
|- ( ( G e. W /\ K e. Z ) -> ( ( G e. USGraph /\ G RegGraph K ) <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |
8 |
3 7
|
bitrd |
|- ( ( G e. W /\ K e. Z ) -> ( G RegUSGraph K <-> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( D ` v ) = K ) ) ) |