Metamath Proof Explorer


Theorem clnbgr0vtx

Description: In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion clnbgr0vtx Vtx G = G ClNeighbVtx K =

Proof

Step Hyp Ref Expression
1 nel02 Vtx G = ¬ K Vtx G
2 df-nel K Vtx G ¬ K Vtx G
3 1 2 sylibr Vtx G = K Vtx G
4 eqid Vtx G = Vtx G
5 4 clnbgrnvtx0 K Vtx G G ClNeighbVtx K =
6 3 5 syl Vtx G = G ClNeighbVtx K =