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

Definition df-haus 17371
 Description: Define the class of all Hausdorff spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.)
Assertion
Ref Expression
df-haus
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-haus
StepHypRef Expression
1 cha 17364 . 2
2 vx . . . . . . . 8
32cv 1651 . . . . . . 7
4 vy . . . . . . . 8
54cv 1651 . . . . . . 7
63, 5wne 2598 . . . . . 6
7 vn . . . . . . . . . 10
82, 7wel 1726 . . . . . . . . 9
9 vm . . . . . . . . . 10
104, 9wel 1726 . . . . . . . . 9
117cv 1651 . . . . . . . . . . 11
129cv 1651 . . . . . . . . . . 11
1311, 12cin 3311 . . . . . . . . . 10
14 c0 3620 . . . . . . . . . 10
1513, 14wceq 1652 . . . . . . . . 9
168, 10, 15w3a 936 . . . . . . . 8
17 vj . . . . . . . . 9
1817cv 1651 . . . . . . . 8
1916, 9, 18wrex 2698 . . . . . . 7
2019, 7, 18wrex 2698 . . . . . 6
216, 20wi 4 . . . . 5
2218cuni 4007 . . . . 5
2321, 4, 22wral 2697 . . . 4
2423, 2, 22wral 2697 . . 3
25 ctop 16950 . . 3
2624, 17, 25crab 2701 . 2
271, 26wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  ishaus  17378
 Copyright terms: Public domain W3C validator