Mathbox for Andrew Salmon < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-line3 Structured version   Unicode version

Definition df-line3 27659
 Description: Define the set of all lines. A line is an infinite subset of that satisfies a property. (Contributed by Andrew Salmon, 15-Jul-2012.)
Assertion
Ref Expression
df-line3
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-line3
StepHypRef Expression
1 cline3 27643 . 2
2 c2o 6718 . . . . 5
3 vx . . . . . 6
43cv 1651 . . . . 5
5 cdom 7107 . . . . 5
62, 4, 5wbr 4212 . . . 4
7 vz . . . . . . . . 9
87cv 1651 . . . . . . . 8
9 vy . . . . . . . . 9
109cv 1651 . . . . . . . 8
118, 10wne 2599 . . . . . . 7
1210, 8cptdfc 27641 . . . . . . . . 9
1312crn 4879 . . . . . . . 8
1413, 4wceq 1652 . . . . . . 7
1511, 14wi 4 . . . . . 6
1615, 7, 4wral 2705 . . . . 5
1716, 9, 4wral 2705 . . . 4
186, 17wa 359 . . 3
19 crr3c 27642 . . . 4
2019cpw 3799 . . 3
2118, 3, 20crab 2709 . 2
221, 21wceq 1652 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator