This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfnbgr2

Description: Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypotheses nbgrval.v 
|- V = ( Vtx ` G )
nbgrval.e 
|- E = ( Edg ` G )
Assertion dfnbgr2 
|- ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )

Proof

Step Hyp Ref Expression
1 nbgrval.v 
 |-  V = ( Vtx ` G )
2 nbgrval.e 
 |-  E = ( Edg ` G )
3 1 2 nbgrval 
 |-  ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } )
4 prssg 
 |-  ( ( N e. V /\ n e. _V ) -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
5 4 elvd 
 |-  ( N e. V -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
6 5 bicomd 
 |-  ( N e. V -> ( { N , n } C_ e <-> ( N e. e /\ n e. e ) ) )
7 6 rexbidv 
 |-  ( N e. V -> ( E. e e. E { N , n } C_ e <-> E. e e. E ( N e. e /\ n e. e ) ) )
8 7 rabbidv 
 |-  ( N e. V -> { n e. ( V \ { N } ) | E. e e. E { N , n } C_ e } = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )
9 3 8 eqtrd 
 |-  ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )