Metamath Proof Explorer


Theorem nbusgr

Description: The set of neighbors of an arbitrary class in a simple graph. (Contributed by Alexander van der Vekens, 9-Oct-2017) (Revised by AV, 26-Oct-2020) (Proof shortened by AV, 27-Nov-2020)

Ref Expression
Hypotheses nbuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbusgr ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e 𝐸 = ( Edg ‘ 𝐺 )
3 usgrumgr ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
4 1 2 nbumgr ( 𝐺 ∈ UMGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
5 3 4 syl ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )