Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-transport Structured version   Unicode version

Definition df-transport 30623
 Description: Define the segment transport function. See fvtransport 30625 for an explanation of the function. (Contributed by Scott Fenton, 18-Oct-2013.)
Assertion
Ref Expression
df-transport TransportTo Cgr
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-transport
StepHypRef Expression
1 ctransport 30622 . 2 TransportTo
2 vp . . . . . . . 8
32cv 1436 . . . . . . 7
4 vn . . . . . . . . . 10
54cv 1436 . . . . . . . . 9
6 cee 24805 . . . . . . . . 9
75, 6cfv 5592 . . . . . . . 8
87, 7cxp 4843 . . . . . . 7
93, 8wcel 1867 . . . . . 6
10 vq . . . . . . . 8
1110cv 1436 . . . . . . 7
1211, 8wcel 1867 . . . . . 6
13 c1st 6796 . . . . . . . 8
1411, 13cfv 5592 . . . . . . 7
15 c2nd 6797 . . . . . . . 8
1611, 15cfv 5592 . . . . . . 7
1714, 16wne 2616 . . . . . 6
189, 12, 17w3a 982 . . . . 5
19 vx . . . . . . 7
2019cv 1436 . . . . . 6
21 vr . . . . . . . . . . 11
2221cv 1436 . . . . . . . . . 10
2314, 22cop 3999 . . . . . . . . 9
24 cbtwn 24806 . . . . . . . . 9
2516, 23, 24wbr 4417 . . . . . . . 8
2616, 22cop 3999 . . . . . . . . 9
27 ccgr 24807 . . . . . . . . 9 Cgr
2826, 3, 27wbr 4417 . . . . . . . 8 Cgr
2925, 28wa 370 . . . . . . 7 Cgr
3029, 21, 7crio 6257 . . . . . 6 Cgr
3120, 30wceq 1437 . . . . 5 Cgr
3218, 31wa 370 . . . 4 Cgr
33 cn 10598 . . . 4
3432, 4, 33wrex 2774 . . 3 Cgr
3534, 2, 10, 19coprab 6297 . 2 Cgr
361, 35wceq 1437 1 TransportTo Cgr
 Colors of variables: wff setvar class This definition is referenced by:  funtransport  30624  fvtransport  30625
 Copyright terms: Public domain W3C validator