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 ) } )