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=\mathrm{Vtx}\left(G\right)$$
	dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
	dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	sclnbgrel	$$⊢X\in S\leftrightarrow \left(X\in V\wedge \exists e\in E\left\{N,X\right\}\subseteq e\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		dfsclnbgr2.s	$$⊢S=\left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
3		dfsclnbgr2.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
4	2	eleq2i	$$⊢X\in S\leftrightarrow X\in \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}$$
5		preq2	$$⊢n=X\to \left\{N,n\right\}=\left\{N,X\right\}$$
6	5	sseq1d	$$⊢n=X\to \left(\left\{N,n\right\}\subseteq e\leftrightarrow \left\{N,X\right\}\subseteq e\right)$$
7	6	rexbidv	$$⊢n=X\to \left(\exists e\in E\left\{N,n\right\}\subseteq e\leftrightarrow \exists e\in E\left\{N,X\right\}\subseteq e\right)$$
8	7	elrab	$$⊢X\in \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}\leftrightarrow \left(X\in V\wedge \exists e\in E\left\{N,X\right\}\subseteq e\right)$$
9	4 8	bitri	$$⊢X\in S\leftrightarrow \left(X\in V\wedge \exists e\in E\left\{N,X\right\}\subseteq e\right)$$