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