Theorem 1hegrvtxdg1r

Description: The vertex degree of a graph with one hyperedge, 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, 23-Feb-2021)

	Ref	Expression
Hypotheses	1hegrvtxdg1.a	$$⊢\phi \to A\in X$$
	1hegrvtxdg1.b	$$⊢\phi \to B\in V$$
	1hegrvtxdg1.c	$$⊢\phi \to C\in V$$
	1hegrvtxdg1.n	$$⊢\phi \to B\ne C$$
	1hegrvtxdg1.x	$$⊢\phi \to E\in 𝒫V$$
	1hegrvtxdg1.i	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\left\{⟨A,E⟩\right\}$$
	1hegrvtxdg1.e	$$⊢\phi \to \left\{B,C\right\}\subseteq E$$
	1hegrvtxdg1.v	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$
Assertion	1hegrvtxdg1r	$$⊢\phi \to \mathrm{VtxDeg}\left(G\right)\left(C\right)=1$$

Proof

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