Step |
Hyp |
Ref |
Expression |
1 |
|
uvtxnbgr.v |
|- V = ( Vtx ` G ) |
2 |
1
|
uvtxnbgr |
|- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) ) |
3 |
|
simpl |
|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. V ) |
4 |
|
raleleq |
|- ( ( V \ { N } ) = ( G NeighbVtx N ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) |
5 |
4
|
eqcoms |
|- ( ( G NeighbVtx N ) = ( V \ { N } ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) |
6 |
5
|
adantl |
|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) |
7 |
1
|
uvtxel |
|- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) ) |
8 |
3 6 7
|
sylanbrc |
|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. ( UnivVtx ` G ) ) |
9 |
8
|
ex |
|- ( N e. V -> ( ( G NeighbVtx N ) = ( V \ { N } ) -> N e. ( UnivVtx ` G ) ) ) |
10 |
2 9
|
impbid2 |
|- ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) ) |