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

Theorem ishaus 19950
 Description: Express the predicate " is a Hausdorff space." (Contributed by NM, 8-Mar-2007.)
Hypothesis
Ref Expression
ist0.1
Assertion
Ref Expression
ishaus
Distinct variable groups:   ,   ,,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ishaus
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 unieq 4259 . . . 4
2 ist0.1 . . . 4
31, 2syl6eqr 2516 . . 3
4 rexeq 3055 . . . . . 6
54rexeqbi1dv 3063 . . . . 5
65imbi2d 316 . . . 4
73, 6raleqbidv 3068 . . 3
83, 7raleqbidv 3068 . 2
9 df-haus 19943 . 2
108, 9elrab2 3259 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3a 973   wceq 1395   wcel 1819   wne 2652  wral 2807  wrex 2808   cin 3470  c0 3793  cuni 4251  ctop 19521  cha 19936 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-uni 4252  df-haus 19943 This theorem is referenced by:  hausnei  19956  haustop  19959  ishaus2  19979  cnhaus  19982  dishaus  20010  pthaus  20265  hausdiag  20272  txhaus  20274  xkohaus  20280
 Copyright terms: Public domain W3C validator