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=\mathrm{Vtx}\left(G\right)$$
	clnbgrval.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	dfclnbgr2	Could not format assertion : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbgrval.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		clnbgrval.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1 2	clnbgrval	Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E { N , n } C_ e } ) ) with typecode |-
4		prssg	$$⊢\left(N\in V\wedge n\in \mathrm{V}\right)\to \left(\left(N\in e\wedge n\in e\right)\leftrightarrow \left\{N,n\right\}\subseteq e\right)$$
5	4	elvd	$$⊢N\in V\to \left(\left(N\in e\wedge n\in e\right)\leftrightarrow \left\{N,n\right\}\subseteq e\right)$$
6	5	bicomd	$$⊢N\in V\to \left(\left\{N,n\right\}\subseteq e\leftrightarrow \left(N\in e\wedge n\in e\right)\right)$$
7	6	rexbidv	$$⊢N\in V\to \left(\exists e\in E\left\{N,n\right\}\subseteq e\leftrightarrow \exists e\in E\left(N\in e\wedge n\in e\right)\right)$$
8	7	rabbidv	$$⊢N\in V\to \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}=\left\{n\in V|\exists e\in E\left(N\in e\wedge n\in e\right)\right\}$$
9	8	uneq2d	$$⊢N\in V\to \left\{N\right\}\cup \left\{n\in V|\exists e\in E\left\{N,n\right\}\subseteq e\right\}=\left\{N\right\}\cup \left\{n\in V|\exists e\in E\left(N\in e\wedge n\in e\right)\right\}$$
10	3 9	eqtrd	Could not format ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) ) : No typesetting found for |- ( N e. V -> ( G ClNeighbVtx N ) = ( { N } u. { n e. V | E. e e. E ( N e. e /\ n e. e ) } ) ) with typecode |-