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

Theorem haustop 20127
 Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
Assertion
Ref Expression
haustop

Proof of Theorem haustop
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2404 . . 3
21ishaus 20118 . 2
32simplbi 460 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   w3a 976   wceq 1407   wcel 1844   wne 2600  wral 2756  wrex 2757   cin 3415  c0 3740  cuni 4193  ctop 19688  cha 20104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382 This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-uni 4194  df-haus 20111 This theorem is referenced by:  haust1  20148  resthaus  20164  sshaus  20171  lmmo  20176  hauscmplem  20201  hauscmp  20202  hauslly  20287  hausllycmp  20289  kgenhaus  20339  pthaus  20433  txhaus  20442  xkohaus  20448  haushmph  20587  cmphaushmeo  20595  hausflim  20776  hauspwpwf1  20782  hauspwpwdom  20783  hausflf  20792  cnextfun  20858  cnextfvval  20859  cnextf  20860  cnextcn  20861  cnextfres  20862  qtophaus  28305  ismntop  28469  hausgraph  35549
 Copyright terms: Public domain W3C validator