Metamath Proof Explorer

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 ∈ I | x ⊆ N
Assertion clnbgrvtxedg ⊢ G ∈ UHGraph ∧ E ∈ I ∧ A ∈ 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 ∈ I | x ⊆ N
4 simp2 ⊢ G ∈ UHGraph ∧ E ∈ I ∧ A ∈ E → E ∈ I
5 2 1 clnbgrssedg ⊢ G ∈ UHGraph ∧ E ∈ I ∧ A ∈ E → E ⊆ N
6 sseq1 ⊢ x = E → x ⊆ N ↔ E ⊆ N
7 6 3 elrab2 ⊢ E ∈ K ↔ E ∈ I ∧ E ⊆ N
8 4 5 7 sylanbrc ⊢ G ∈ UHGraph ∧ E ∈ I ∧ A ∈ E → E ∈ K