Metamath Proof Explorer

Theorem clnbgrssedg

Description: The vertices connected by an edge are a subset of the neighborhood 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