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 e. UHGraph /\ K e. E /\ X e. K ) -> K C_ N )

Proof

Step Hyp Ref Expression
1 clnbgrssedg.e
 |-  E = ( Edg ` G )
2 clnbgrssedg.n
 |-  N = ( G ClNeighbVtx X )
3 1 2 clnbgredg
 |-  ( ( G e. UHGraph /\ ( K e. E /\ X e. K /\ v e. K ) ) -> v e. N )
4 3 3exp2
 |-  ( G e. UHGraph -> ( K e. E -> ( X e. K -> ( v e. K -> v e. N ) ) ) )
5 4 3imp
 |-  ( ( G e. UHGraph /\ K e. E /\ X e. K ) -> ( v e. K -> v e. N ) )
6 5 ssrdv
 |-  ( ( G e. UHGraph /\ K e. E /\ X e. K ) -> K C_ N )