Metamath Proof Explorer


Theorem 0conngr

Description: A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

Ref Expression
Assertion 0conngr ConnGraph

Proof

Step Hyp Ref Expression
1 ral0 k n f p f k PathsOn n p
2 0ex V
3 vtxval0 Vtx =
4 3 eqcomi = Vtx
5 4 isconngr V ConnGraph k n f p f k PathsOn n p
6 2 5 ax-mp ConnGraph k n f p f k PathsOn n p
7 1 6 mpbir ConnGraph