Metamath Proof Explorer


Theorem ist1

Description: The predicate "is a T_1 space". (Contributed by FL, 18-Jun-2007)

Ref Expression
Hypothesis ist0.1 X = J
Assertion ist1 J Fre J Top a X a Clsd J

Proof

Step Hyp Ref Expression
1 ist0.1 X = J
2 unieq x = J x = J
3 2 1 eqtr4di x = J x = X
4 fveq2 x = J Clsd x = Clsd J
5 4 eleq2d x = J a Clsd x a Clsd J
6 3 5 raleqbidv x = J a x a Clsd x a X a Clsd J
7 df-t1 Fre = x Top | a x a Clsd x
8 6 7 elrab2 J Fre J Top a X a Clsd J