Theorem sclnbgrelself

Description: A vertex N is a member of its semiclosed neighborhood iff there is an edge joining the vertex with a vertex. (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	sclnbgrelself	|- ( N e. S <-> ( N e. V /\ E. e 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	1 2 3	sclnbgrel	|- ( N e. S <-> ( N e. V /\ E. e e. E { N , N } C_ e ) )
5		dfsn2	|- { N } = { N , N }
6	5	eqcomi	|- { N , N } = { N }
7	6	sseq1i	|- ( { N , N } C_ e <-> { N } C_ e )
8		snssg	|- ( N e. V -> ( N e. e <-> { N } C_ e ) )
9	7 8	bitr4id	|- ( N e. V -> ( { N , N } C_ e <-> N e. e ) )
10	9	rexbidv	|- ( N e. V -> ( E. e e. E { N , N } C_ e <-> E. e e. E N e. e ) )
11	10	pm5.32i	|- ( ( N e. V /\ E. e e. E { N , N } C_ e ) <-> ( N e. V /\ E. e e. E N e. e ) )
12	4 11	bitri	|- ( N e. S <-> ( N e. V /\ E. e e. E N e. e ) )