Metamath Proof Explorer


Theorem uvtxnbgr

Description: A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017) (Revised by AV, 3-Nov-2020) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypothesis uvtxnbgr.v
|- V = ( Vtx ` G )
Assertion uvtxnbgr
|- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) )

Proof

Step Hyp Ref Expression
1 uvtxnbgr.v
 |-  V = ( Vtx ` G )
2 1 nbgrssovtx
 |-  ( G NeighbVtx N ) C_ ( V \ { N } )
3 2 a1i
 |-  ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) C_ ( V \ { N } ) )
4 1 uvtxnbgrss
 |-  ( N e. ( UnivVtx ` G ) -> ( V \ { N } ) C_ ( G NeighbVtx N ) )
5 3 4 eqssd
 |-  ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) )