Metamath Proof Explorer


Theorem dfnbgr2

Description: Alternate definition of the neighbors of a vertex breaking up the subset relationship of an unordered pair. (Contributed by AV, 15-Nov-2020) (Revised by AV, 21-Mar-2021)

Ref Expression
Hypotheses nbgrval.v V = Vtx G
nbgrval.e E = Edg G
Assertion dfnbgr2 N V G NeighbVtx N = n V N | e E N e n e

Proof

Step Hyp Ref Expression
1 nbgrval.v V = Vtx G
2 nbgrval.e E = Edg G
3 1 2 nbgrval N V G NeighbVtx N = n V N | 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 N | e E N n e = n V N | e E N e n e
9 3 8 eqtrd N V G NeighbVtx N = n V N | e E N e n e