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