Metamath Proof Explorer


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 = Vtx G
clnbgrval.e E = Edg G
Assertion dfclnbgr2 N V G ClNeighbVtx N = N n V | e E N e n e

Proof

Step Hyp Ref Expression
1 clnbgrval.v V = Vtx G
2 clnbgrval.e E = Edg G
3 1 2 clnbgrval N V G ClNeighbVtx N = N n V | e E N n e
4 prssg N V n V N e n e N n e
5 4 elvd N V N e n e N n e
6 5 bicomd N V N n e N e n e
7 6 rexbidv N V e E N n e e E N e n e
8 7 rabbidv N V n V | e E N n e = n V | e E N e n e
9 8 uneq2d N V N n V | e E N n e = N n V | e E N e n e
10 3 9 eqtrd N V G ClNeighbVtx N = N n V | e E N e n e