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

Definition df-1stc 20066
 Description: Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
Assertion
Ref Expression
df-1stc
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-1stc
StepHypRef Expression
1 c1stc 20064 . 2
2 vy . . . . . . . 8
32cv 1394 . . . . . . 7
4 com 6699 . . . . . . 7
5 cdom 7533 . . . . . . 7
63, 4, 5wbr 4456 . . . . . 6
7 vx . . . . . . . . 9
8 vz . . . . . . . . 9
97, 8wel 1820 . . . . . . . 8
107cv 1394 . . . . . . . . 9
118cv 1394 . . . . . . . . . . . 12
1211cpw 4015 . . . . . . . . . . 11
133, 12cin 3470 . . . . . . . . . 10
1413cuni 4251 . . . . . . . . 9
1510, 14wcel 1819 . . . . . . . 8
169, 15wi 4 . . . . . . 7
17 vj . . . . . . . 8
1817cv 1394 . . . . . . 7
1916, 8, 18wral 2807 . . . . . 6
206, 19wa 369 . . . . 5
2118cpw 4015 . . . . 5
2220, 2, 21wrex 2808 . . . 4
2318cuni 4251 . . . 4
2422, 7, 23wral 2807 . . 3
25 ctop 19521 . . 3
2624, 17, 25crab 2811 . 2
271, 26wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  is1stc  20068
 Copyright terms: Public domain W3C validator