Theorem vtxdusgradjvtx

Description: The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018) (Revised by AV, 23-Dec-2020)

	Ref	Expression
Hypotheses	vtxdusgradjvtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	vtxdusgradjvtx.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	vtxdusgradjvtx	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=\left|\left\{v\in V|\left\{U,v\right\}\in E\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		vtxdusgradjvtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		vtxdusgradjvtx.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3	1	hashnbusgrvd	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left|G\mathrm{NeighbVtx}U\right|=\mathrm{VtxDeg}\left(G\right)\left(U\right)$$
4	1 2	nbusgrvtx	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to G\mathrm{NeighbVtx}U=\left\{v\in V|\left\{U,v\right\}\in E\right\}$$
5	4	fveq2d	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \left|G\mathrm{NeighbVtx}U\right|=\left|\left\{v\in V|\left\{U,v\right\}\in E\right\}\right|$$
6	3 5	eqtr3d	$$⊢\left(G\in \mathrm{USGraph}\wedge U\in V\right)\to \mathrm{VtxDeg}\left(G\right)\left(U\right)=\left|\left\{v\in V|\left\{U,v\right\}\in E\right\}\right|$$