Theorem clnbgrvtxedg

Description: An edge E containing a vertex A is an edge in the closed neighborhood of this vertex A . (Contributed by AV, 25-Dec-2025)

	Ref	Expression
Hypotheses	clnbgrvtxedg.n	|- N = ( G ClNeighbVtx A )
	clnbgrvtxedg.i	|- I = ( Edg ` G )
	clnbgrvtxedg.k	|- K = { x e. I | x C_ N }
Assertion	clnbgrvtxedg	|- ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E e. K )

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxedg.n	|- N = ( G ClNeighbVtx A )
2		clnbgrvtxedg.i	|- I = ( Edg ` G )
3		clnbgrvtxedg.k	|- K = { x e. I | x C_ N }
4		simp2	|- ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E e. I )
5	2 1	clnbgrssedg	|- ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E C_ N )
6		sseq1	|- ( x = E -> ( x C_ N <-> E C_ N ) )
7	6 3	elrab2	|- ( E e. K <-> ( E e. I /\ E C_ N ) )
8	4 5 7	sylanbrc	|- ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E e. K )