Theorem sclnbgrel

Description: Characterization of a member X of the semiclosed neighborhood of a vertex N in a graph G . (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	sclnbgrel	|- ( X e. S <-> ( X e. V /\ E. e e. E { N , X } C_ 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	2	eleq2i	|- ( X e. S <-> X e. { n e. V | E. e e. E { N , n } C_ e } )
5		preq2	|- ( n = X -> { N , n } = { N , X } )
6	5	sseq1d	|- ( n = X -> ( { N , n } C_ e <-> { N , X } C_ e ) )
7	6	rexbidv	|- ( n = X -> ( E. e e. E { N , n } C_ e <-> E. e e. E { N , X } C_ e ) )
8	7	elrab	|- ( X e. { n e. V | E. e e. E { N , n } C_ e } <-> ( X e. V /\ E. e e. E { N , X } C_ e ) )
9	4 8	bitri	|- ( X e. S <-> ( X e. V /\ E. e e. E { N , X } C_ e ) )