Metamath Proof Explorer


Theorem ishaus

Description: The predicate "is a Hausdorff space". (Contributed by NM, 8-Mar-2007)

Ref Expression
Hypothesis ist0.1 X = J
Assertion ishaus J Haus J Top x X y X x y n J m J x n y m n m =

Proof

Step Hyp Ref Expression
1 ist0.1 X = J
2 unieq j = J j = J
3 2 1 syl6eqr j = J j = X
4 rexeq j = J m j x n y m n m = m J x n y m n m =
5 4 rexeqbi1dv j = J n j m j x n y m n m = n J m J x n y m n m =
6 5 imbi2d j = J x y n j m j x n y m n m = x y n J m J x n y m n m =
7 3 6 raleqbidv j = J y j x y n j m j x n y m n m = y X x y n J m J x n y m n m =
8 3 7 raleqbidv j = J x j y j x y n j m j x n y m n m = x X y X x y n J m J x n y m n m =
9 df-haus Haus = j Top | x j y j x y n j m j x n y m n m =
10 8 9 elrab2 J Haus J Top x X y X x y n J m J x n y m n m =