Database
GRAPH THEORY
Undirected graphs
Vertex degree
1egrvtxdg1r
Metamath Proof Explorer
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