Metamath Proof Explorer


Theorem clnbgrprc0

Description: The closed neighborhood is empty if the graph G or the vertex N are proper classes. (Contributed by AV, 7-May-2025)

Ref Expression
Assertion clnbgrprc0 ¬ G V N V G ClNeighbVtx N =

Proof

Step Hyp Ref Expression
1 df-clnbgr ClNeighbVtx = g V , v Vtx g v n Vtx g | e Edg g v n e
2 1 reldmmpo Rel dom ClNeighbVtx
3 2 ovprc ¬ G V N V G ClNeighbVtx N =