Metamath Proof Explorer

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 = Vtx ⁡ G
vtxdusgradjvtx.e ⊢ E = Edg ⁡ G
Assertion vtxdusgradjvtx ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = v ∈ V | U v ∈ E

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ⊢ V = Vtx ⁡ G
2 vtxdusgradjvtx.e ⊢ E = Edg ⁡ G
3 1 hashnbusgrvd ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = VtxDeg ⁡ G ⁡ U
4 1 2 nbusgrvtx ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = v ∈ V | U v ∈ E
5 4 fveq2d ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = v ∈ V | U v ∈ E
6 3 5 eqtr3d ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = v ∈ V | U v ∈ E