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

Definition df-1stc 19143
 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 19141 . 2
2 vy . . . . . . . 8
32cv 1369 . . . . . . 7
4 com 6560 . . . . . . 7
5 cdom 7392 . . . . . . 7
63, 4, 5wbr 4374 . . . . . 6
7 vx . . . . . . . . 9
8 vz . . . . . . . . 9
97, 8wel 1758 . . . . . . . 8
107cv 1369 . . . . . . . . 9
118cv 1369 . . . . . . . . . . . 12
1211cpw 3942 . . . . . . . . . . 11
133, 12cin 3409 . . . . . . . . . 10
1413cuni 4173 . . . . . . . . 9
1510, 14wcel 1757 . . . . . . . 8
169, 15wi 4 . . . . . . 7
17 vj . . . . . . . 8
1817cv 1369 . . . . . . 7
1916, 8, 18wral 2792 . . . . . 6
206, 19wa 369 . . . . 5
2118cpw 3942 . . . . 5
2220, 2, 21wrex 2793 . . . 4
2318cuni 4173 . . . 4
2422, 7, 23wral 2792 . . 3
25 ctop 18598 . . 3
2624, 17, 25crab 2796 . 2
271, 26wceq 1370 1
 Colors of variables: wff setvar class This definition is referenced by:  is1stc  19145
 Copyright terms: Public domain W3C validator