Theorem dfsclnbgr2

Description: Alternate definition of the semiclosed neighborhood of a vertex breaking up the subset relationship of an unordered pair. Asemiclosed neighborhood S of a vertex N is the set of all vertices incident with edges which join the vertex N with a vertex. Therefore, a vertex is contained in its semiclosed neighborhood if it is connected with any vertex by an edge (see sclnbgrelself ), even only with itself (i.e., by a loop). (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	dfsclnbgr2	|- ( N e. V -> S = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )

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		prssg	|- ( ( N e. V /\ n e. V ) -> ( ( N e. e /\ n e. e ) <-> { N , n } C_ e ) )
5	4	bicomd	|- ( ( N e. V /\ n e. V ) -> ( { N , n } C_ e <-> ( N e. e /\ n e. e ) ) )
6	5	rexbidv	|- ( ( N e. V /\ n e. V ) -> ( E. e e. E { N , n } C_ e <-> E. e e. E ( N e. e /\ n e. e ) ) )
7	6	rabbidva	|- ( 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 ) } )
8	2 7	eqtrid	|- ( N e. V -> S = { n e. V | E. e e. E ( N e. e /\ n e. e ) } )