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→GNeighbVtxN=n∈V∖N|∃e∈EN∈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→GNeighbVtxN=n∈V∖N|∃e∈ENn⊆e
4 prssg ⊢N∈V∧n∈V→N∈e∧n∈e↔Nn⊆e
5 4 elvd ⊢N∈V→N∈e∧n∈e↔Nn⊆e
6 5 bicomd ⊢N∈V→Nn⊆e↔N∈e∧n∈e
7 6 rexbidv ⊢N∈V→∃e∈ENn⊆e↔∃e∈EN∈e∧n∈e
8 7 rabbidv ⊢N∈V→n∈V∖N|∃e∈ENn⊆e=n∈V∖N|∃e∈EN∈e∧n∈e
9 3 8 eqtrd ⊢N∈V→GNeighbVtxN=n∈V∖N|∃e∈EN∈e∧n∈e