Theorem dfclnbgr2

Description: Alternate definition of the closed neighborhood of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 7-May-2025)

	Ref	Expression
Hypotheses	clnbgrval.v	|- V = ( Vtx ` G )
	clnbgrval.e	|- E = ( Edg ` G )
Assertion	dfclnbgr2	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrval.v	|- V = ( Vtx ` G )
2		clnbgrval.e	|- E = ( Edg ` G )
3	1 2	clnbgrval	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | 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 | E. e e. E { N , n } C_ e } = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )
9	8	uneq2d	|- ( N e. V -> ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )
10	3 9	eqtrd	|- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) )