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

Definition df-2spthonot 25159
 Description: Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.)
Assertion
Ref Expression
df-2spthonot 2SPathOnOt SPathOn
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-2spthonot
StepHypRef Expression
1 c2pthonot 25156 . 2 2SPathOnOt
2 vv . . 3
3 ve . . 3
4 cvv 3056 . . 3
5 va . . . 4
6 vb . . . 4
72cv 1402 . . . 4
8 vf . . . . . . . . . 10
98cv 1402 . . . . . . . . 9
10 vp . . . . . . . . . 10
1110cv 1402 . . . . . . . . 9
125cv 1402 . . . . . . . . . 10
136cv 1402 . . . . . . . . . 10
143cv 1402 . . . . . . . . . . 11
15 cspthon 24804 . . . . . . . . . . 11 SPathOn
167, 14, 15co 6232 . . . . . . . . . 10 SPathOn
1712, 13, 16co 6232 . . . . . . . . 9 SPathOn
189, 11, 17wbr 4392 . . . . . . . 8 SPathOn
19 chash 12357 . . . . . . . . . 10
209, 19cfv 5523 . . . . . . . . 9
21 c2 10544 . . . . . . . . 9
2220, 21wceq 1403 . . . . . . . 8
23 vt . . . . . . . . . . . . 13
2423cv 1402 . . . . . . . . . . . 12
25 c1st 6734 . . . . . . . . . . . 12
2624, 25cfv 5523 . . . . . . . . . . 11
2726, 25cfv 5523 . . . . . . . . . 10
2827, 12wceq 1403 . . . . . . . . 9
29 c2nd 6735 . . . . . . . . . . 11
3026, 29cfv 5523 . . . . . . . . . 10
31 c1 9441 . . . . . . . . . . 11
3231, 11cfv 5523 . . . . . . . . . 10
3330, 32wceq 1403 . . . . . . . . 9
3424, 29cfv 5523 . . . . . . . . . 10
3534, 13wceq 1403 . . . . . . . . 9
3628, 33, 35w3a 972 . . . . . . . 8
3718, 22, 36w3a 972 . . . . . . 7 SPathOn
3837, 10wex 1631 . . . . . 6 SPathOn
3938, 8wex 1631 . . . . 5 SPathOn
407, 7cxp 4938 . . . . . 6
4140, 7cxp 4938 . . . . 5
4239, 23, 41crab 2755 . . . 4 SPathOn
435, 6, 7, 7, 42cmpt2 6234 . . 3 SPathOn
442, 3, 4, 4, 43cmpt2 6234 . 2 SPathOn
451, 44wceq 1403 1 2SPathOnOt SPathOn
 Colors of variables: wff setvar class This definition is referenced by:  is2spthonot  25163  2spthonot3v  25175
 Copyright terms: Public domain W3C validator