Metamath Proof Explorer

Theorem 0grrgr

Description: The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020)

Ref Expression
Assertion 0grrgr 
|- A. k e. NN0* (/) RegGraph k

Proof

Step Hyp Ref Expression
1 0grrusgr 
 |-  A. k e. NN0* (/) RegUSGraph k
2 rusgrrgr 
 |-  ( (/) RegUSGraph k -> (/) RegGraph k )
3 2 ralimi 
 |-  ( A. k e. NN0* (/) RegUSGraph k -> A. k e. NN0* (/) RegGraph k )
4 1 3 ax-mp 
 |-  A. k e. NN0* (/) RegGraph k