Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  haust1 Structured version   Visualization version   Unicode version

Theorem haust1 20368
 Description: A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
Assertion
Ref Expression
haust1

Proof of Theorem haust1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2451 . . . . . . . . 9
21hausnei 20344 . . . . . . . 8
3 simprr1 1056 . . . . . . . . . . 11
4 noel 3735 . . . . . . . . . . . . 13
5 simprr3 1058 . . . . . . . . . . . . . 14
65eleq2d 2514 . . . . . . . . . . . . 13
74, 6mtbiri 305 . . . . . . . . . . . 12
8 simprr2 1057 . . . . . . . . . . . . 13
9 elin 3617 . . . . . . . . . . . . . 14
109simplbi2com 633 . . . . . . . . . . . . 13
118, 10syl 17 . . . . . . . . . . . 12
127, 11mtod 181 . . . . . . . . . . 11
133, 12jca 535 . . . . . . . . . 10
1413rexlimdvaa 2880 . . . . . . . . 9
1514reximdva 2862 . . . . . . . 8
162, 15mpd 15 . . . . . . 7
17 rexanali 2840 . . . . . . 7
1816, 17sylib 200 . . . . . 6
19183exp2 1227 . . . . 5
2019imp32 435 . . . 4