This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1egrvtxdg1r

Description: The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

Ref Expression
Hypotheses 1egrvtxdg1.v ⊢ φ → Vtx ⁡ G = V
1egrvtxdg1.a ⊢ φ → A ∈ X
1egrvtxdg1.b ⊢ φ → B ∈ V
1egrvtxdg1.c ⊢ φ → C ∈ V
1egrvtxdg1.n ⊢ φ → B ≠ C
1egrvtxdg1.i ⊢ φ → iEdg ⁡ G = A B C
Assertion 1egrvtxdg1r ⊢ φ → VtxDeg ⁡ G ⁡ C = 1

Proof

Step Hyp Ref Expression
1 1egrvtxdg1.v ⊢ φ → Vtx ⁡ G = V
2 1egrvtxdg1.a ⊢ φ → A ∈ X
3 1egrvtxdg1.b ⊢ φ → B ∈ V
4 1egrvtxdg1.c ⊢ φ → C ∈ V
5 1egrvtxdg1.n ⊢ φ → B ≠ C
6 1egrvtxdg1.i ⊢ φ → iEdg ⁡ G = A B C
7 5 necomd ⊢ φ → C ≠ B
8 prcom ⊢ B C = C B
9 8 a1i ⊢ φ → B C = C B
10 9 opeq2d ⊢ φ → A B C = A C B
11 10 sneqd ⊢ φ → A B C = A C B
12 6 11 eqtrd ⊢ φ → iEdg ⁡ G = A C B
13 1 2 4 3 7 12 1egrvtxdg1 ⊢ φ → VtxDeg ⁡ G ⁡ C = 1