Metamath Proof Explorer


Theorem clnbgrssedg

Description: The vertices connected by an edge are a subset of the neigborhood of each of these vertices. (Contributed by AV, 26-May-2025) (Proof shortened by AV, 24-Aug-2025)

Ref Expression
Hypotheses clnbgrssedg.e E = Edg G
clnbgrssedg.n N = G ClNeighbVtx X
Assertion clnbgrssedg G UHGraph K E X K K N

Proof

Step Hyp Ref Expression
1 clnbgrssedg.e E = Edg G
2 clnbgrssedg.n N = G ClNeighbVtx X
3 1 2 clnbgredg G UHGraph K E X K v K v N
4 3 3exp2 G UHGraph K E X K v K v N
5 4 3imp G UHGraph K E X K v K v N
6 5 ssrdv G UHGraph K E X K K N