Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdgrfval Structured version   Unicode version

Theorem vdgrfval 21667
 Description: The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
Assertion
Ref Expression
vdgrfval VDeg
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,

Proof of Theorem vdgrfval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-vdgr 21666 . . 3 VDeg
21a1i 11 . 2 VDeg
3 simprl 734 . . 3
4 simprr 735 . . . . . . . 8
54dmeqd 5073 . . . . . . 7
6 simpl2 962 . . . . . . . 8
7 fndm 5545 . . . . . . . 8
86, 7syl 16 . . . . . . 7
95, 8eqtrd 2469 . . . . . 6
104fveq1d 5731 . . . . . . 7
1110eleq2d 2504 . . . . . 6
129, 11rabeqbidv 2952 . . . . 5
1312fveq2d 5733 . . . 4
1410eqeq1d 2445 . . . . . 6
159, 14rabeqbidv 2952 . . . . 5
1615fveq2d 5733 . . . 4
1713, 16oveq12d 6100 . . 3
183, 17mpteq12dv 4288 . 2
19 elex 2965 . . 3