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	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
	1egrvtxdg1.a	$$⊢\phi \to A\in X$$
	1egrvtxdg1.b	$$⊢\phi \to B\in V$$
	1egrvtxdg1.c	$$⊢\phi \to C\in V$$
	1egrvtxdg1.n	$$⊢\phi \to B\ne C$$
	1egrvtxdg1.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{B,C\right\}⟩\right\}$$
Assertion	1egrvtxdg1r	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(C\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
2		1egrvtxdg1.a	$$⊢\phi \to A\in X$$
3		1egrvtxdg1.b	$$⊢\phi \to B\in V$$
4		1egrvtxdg1.c	$$⊢\phi \to C\in V$$
5		1egrvtxdg1.n	$$⊢\phi \to B\ne C$$
6		1egrvtxdg1.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{B,C\right\}⟩\right\}$$
7	5	necomd	$$⊢\phi \to C\ne B$$
8		prcom	$$⊢\left\{B,C\right\}=\left\{C,B\right\}$$
9	8	a1i	$$⊢\phi \to \left\{B,C\right\}=\left\{C,B\right\}$$
10	9	opeq2d	$$⊢\phi \to ⟨A,\left\{B,C\right\}⟩=⟨A,\left\{C,B\right\}⟩$$
11	10	sneqd	$$⊢\phi \to \left\{⟨A,\left\{B,C\right\}⟩\right\}=\left\{⟨A,\left\{C,B\right\}⟩\right\}$$
12	6 11	eqtrd	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,\left\{C,B\right\}⟩\right\}$$
13	1 2 4 3 7 12	1egrvtxdg1	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(C\right)=1$$