Metamath Proof Explorer

Theorem nbgrprc0

Description: The set of neighbors is empty if the graph G or the vertex N are proper classes. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion nbgrprc0 ⊢¬G∈V∧N∈V→GNeighbVtxN=∅

Proof

Step Hyp Ref Expression
1 df-nbgr ⊢NeighbVtx=g∈V,v∈Vtx⁡g⟼n∈Vtx⁡g∖v|∃e∈Edg⁡gvn⊆e
2 1 reldmmpo ⊢Rel⁡dom⁡NeighbVtx
3 2 ovprc ⊢¬G∈V∧N∈V→GNeighbVtxN=∅