Theorem dfnbgr5

Description: Alternate definition of the (open) neighborhood of a vertex as a semiclosed neighborhood without itself. (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	|- V = ( Vtx ` G )
	dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
	dfsclnbgr2.e	|- E = ( Edg ` G )
Assertion	dfnbgr5	|- ( N e. V -> ( G NeighbVtx N ) = ( S \ { N } ) )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	|- V = ( Vtx ` G )
2		dfsclnbgr2.s	|- S = { n e. V | E. e e. E { N , n } C_ e }
3		dfsclnbgr2.e	|- E = ( Edg ` G )
4		rabdif	|- ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) }
5	4	eqcomi	|- { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } = ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } )
6	1 3	dfnbgr2	|- ( N e. V -> ( G NeighbVtx N ) = { n e. ( V \ { N } ) | E. e e. E ( N e. e /\ n e. e ) } )
7	1 2 3	dfsclnbgr2	|- ( N e. V -> S = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )
8	7	difeq1d	|- ( N e. V -> ( S \ { N } ) = ( { n e. V | E. e e. E ( N e. e /\ n e. e ) } \ { N } ) )
9	5 6 8	3eqtr4a	|- ( N e. V -> ( G NeighbVtx N ) = ( S \ { N } ) )