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 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 )