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

Definition df-transport 25956
 Description: Define the segment transport function. See fvtransport 25958 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 25955 . 2 TransportTo
2 vp . . . . . . . 8
32cv 1651 . . . . . . 7
4 vn . . . . . . . . . 10
54cv 1651 . . . . . . . . 9
6 cee 25819 . . . . . . . . 9
75, 6cfv 5446 . . . . . . . 8
87, 7cxp 4868 . . . . . . 7
93, 8wcel 1725 . . . . . 6
10 vq . . . . . . . 8
1110cv 1651 . . . . . . 7
1211, 8wcel 1725 . . . . . 6
13 c1st 6339 . . . . . . . 8
1411, 13cfv 5446 . . . . . . 7
15 c2nd 6340 . . . . . . . 8
1611, 15cfv 5446 . . . . . . 7
1714, 16wne 2598 . . . . . 6
189, 12, 17w3a 936 . . . . 5
19 vx . . . . . . 7
2019cv 1651 . . . . . 6
21 vr . . . . . . . . . . 11
2221cv 1651 . . . . . . . . . 10
2314, 22cop 3809 . . . . . . . . 9
24 cbtwn 25820 . . . . . . . . 9
2516, 23, 24wbr 4204 . . . . . . . 8
2616, 22cop 3809 . . . . . . . . 9
27 ccgr 25821 . . . . . . . . 9 Cgr
2826, 3, 27wbr 4204 . . . . . . . 8 Cgr
2925, 28wa 359 . . . . . . 7 Cgr
3029, 21, 7crio 6534 . . . . . 6 Cgr
3120, 30wceq 1652 . . . . 5 Cgr
3218, 31wa 359 . . . 4 Cgr
33 cn 9992 . . . 4
3432, 4, 33wrex 2698 . . 3 Cgr
3534, 2, 10, 19coprab 6074 . 2 Cgr
361, 35wceq 1652 1 TransportTo Cgr
 Colors of variables: wff set class This definition is referenced by:  funtransport  25957  fvtransport  25958
 Copyright terms: Public domain W3C validator