Theorem nbusgrvtx

Description: The set of neighbors of a vertex 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	nbusgrvtx	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )

Proof

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