Metamath Proof Explorer


Theorem clnbgr0edg

Description: In an empty graph (with no edges), all closed neighborhoods consists of a single vertex. (Contributed by AV, 10-May-2025)

Ref Expression
Assertion clnbgr0edg Edg G = K Vtx G G ClNeighbVtx K = K

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 1 dfclnbgr4 K Vtx G G ClNeighbVtx K = K G NeighbVtx K
3 2 adantl Edg G = K Vtx G G ClNeighbVtx K = K G NeighbVtx K
4 nbgr0edg Edg G = G NeighbVtx K =
5 4 adantr Edg G = K Vtx G G NeighbVtx K =
6 5 uneq2d Edg G = K Vtx G K G NeighbVtx K = K
7 un0 K = K
8 7 a1i Edg G = K Vtx G K = K
9 3 6 8 3eqtrd Edg G = K Vtx G G ClNeighbVtx K = K