Metamath Proof Explorer


Theorem wlk0prc

Description: There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

Ref Expression
Assertion wlk0prc S V Vtx S = Vtx G Walks G =

Proof

Step Hyp Ref Expression
1 eqcom Vtx S = Vtx G Vtx G = Vtx S
2 1 biimpi Vtx S = Vtx G Vtx G = Vtx S
3 vtxvalprc S V Vtx S =
4 2 3 sylan9eqr S V Vtx S = Vtx G Vtx G =
5 g0wlk0 Vtx G = Walks G =
6 4 5 syl S V Vtx S = Vtx G Walks G =