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

Definition df-haus 17333
 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 17326 . 2
2 vx . . . . . . . 8
32cv 1648 . . . . . . 7
4 vy . . . . . . . 8
54cv 1648 . . . . . . 7
63, 5wne 2567 . . . . . 6
7 vn . . . . . . . . . 10
82, 7wel 1722 . . . . . . . . 9
9 vm . . . . . . . . . 10
104, 9wel 1722 . . . . . . . . 9
117cv 1648 . . . . . . . . . . 11
129cv 1648 . . . . . . . . . . 11
1311, 12cin 3279 . . . . . . . . . 10
14 c0 3588 . . . . . . . . . 10
1513, 14wceq 1649 . . . . . . . . 9
168, 10, 15w3a 936 . . . . . . . 8
17 vj . . . . . . . . 9
1817cv 1648 . . . . . . . 8
1916, 9, 18wrex 2667 . . . . . . 7
2019, 7, 18wrex 2667 . . . . . 6
216, 20wi 4 . . . . 5
2218cuni 3975 . . . . 5
2321, 4, 22wral 2666 . . . 4
2423, 2, 22wral 2666 . . 3
25 ctop 16913 . . 3
2624, 17, 25crab 2670 . 2
271, 26wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  ishaus  17340
 Copyright terms: Public domain W3C validator