Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-spthon Unicode version

Definition df-spthon 21478
 Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
Assertion
Ref Expression
df-spthon SPathOn WalkOn SPaths
Distinct variable groups:   ,,,   ,,,,,

Detailed syntax breakdown of Definition df-spthon
StepHypRef Expression
1 cspthon 21466 . 2 SPathOn
2 vv . . 3
3 ve . . 3
4 cvv 2916 . . 3
5 va . . . 4
6 vb . . . 4
72cv 1648 . . . 4
8 vf . . . . . . . 8
98cv 1648 . . . . . . 7
10 vp . . . . . . . 8
1110cv 1648 . . . . . . 7
125cv 1648 . . . . . . . 8
136cv 1648 . . . . . . . 8
143cv 1648 . . . . . . . . 9
15 cwlkon 21463 . . . . . . . . 9 WalkOn
167, 14, 15co 6040 . . . . . . . 8 WalkOn
1712, 13, 16co 6040 . . . . . . 7 WalkOn
189, 11, 17wbr 4172 . . . . . 6 WalkOn
19 cspath 21462 . . . . . . . 8 SPaths
207, 14, 19co 6040 . . . . . . 7 SPaths
219, 11, 20wbr 4172 . . . . . 6 SPaths
2218, 21wa 359 . . . . 5 WalkOn SPaths
2322, 8, 10copab 4225 . . . 4 WalkOn SPaths
245, 6, 7, 7, 23cmpt2 6042 . . 3 WalkOn SPaths
252, 3, 4, 4, 24cmpt2 6042 . 2 WalkOn SPaths
261, 25wceq 1649 1 SPathOn WalkOn SPaths
 Colors of variables: wff set class This definition is referenced by:  spthon  21535  spthonprp  21538
 Copyright terms: Public domain W3C validator