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	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
	clnbgrvtxedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
	clnbgrvtxedg.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
Assertion	clnbgrvtxedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxedg.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
2		clnbgrvtxedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
3		clnbgrvtxedg.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
4		simp2	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ 𝐼 )
5	2 1	clnbgrssedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ⊆ 𝑁 )
6		sseq1	⊢ ( 𝑥 = 𝐸 → ( 𝑥 ⊆ 𝑁 ↔ 𝐸 ⊆ 𝑁 ) )
7	6 3	elrab2	⊢ ( 𝐸 ∈ 𝐾 ↔ ( 𝐸 ∈ 𝐼 ∧ 𝐸 ⊆ 𝑁 ) )
8	4 5 7	sylanbrc	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ 𝐾 )