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

Definition df-1stc 17502
 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 17500 . 2
2 vy . . . . . . . 8
32cv 1651 . . . . . . 7
4 com 4845 . . . . . . 7
5 cdom 7107 . . . . . . 7
63, 4, 5wbr 4212 . . . . . 6
7 vx . . . . . . . . 9
8 vz . . . . . . . . 9
97, 8wel 1726 . . . . . . . 8
107cv 1651 . . . . . . . . 9
118cv 1651 . . . . . . . . . . . 12
1211cpw 3799 . . . . . . . . . . 11
133, 12cin 3319 . . . . . . . . . 10
1413cuni 4015 . . . . . . . . 9
1510, 14wcel 1725 . . . . . . . 8
169, 15wi 4 . . . . . . 7
17 vj . . . . . . . 8
1817cv 1651 . . . . . . 7
1916, 8, 18wral 2705 . . . . . 6
206, 19wa 359 . . . . 5
2118cpw 3799 . . . . 5
2220, 2, 21wrex 2706 . . . 4
2318cuni 4015 . . . 4
2422, 7, 23wral 2705 . . 3
25 ctop 16958 . . 3
2624, 17, 25crab 2709 . 2
271, 26wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  is1stc  17504
 Copyright terms: Public domain W3C validator