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

Definition df-hmph 20708
Description: Definition of the relation  x is homeomorphic to  y. (Contributed by FL, 14-Feb-2007.)
Assertion
Ref Expression
df-hmph  |-  ~=  =  ( `' Homeo " ( _V  \  1o ) )

Detailed syntax breakdown of Definition df-hmph
StepHypRef Expression
1 chmph 20706 . 2  class  ~=
2 chmeo 20705 . . . 4  class  Homeo
32ccnv 4844 . . 3  class  `' Homeo
4 cvv 3078 . . . 4  class  _V
5 c1o 7174 . . . 4  class  1o
64, 5cdif 3430 . . 3  class  ( _V 
\  1o )
73, 6cima 4848 . 2  class  ( `'
Homeo " ( _V  \  1o ) )
81, 7wceq 1437 1  wff  ~=  =  ( `' Homeo " ( _V  \  1o ) )
Colors of variables: wff setvar class
This definition is referenced by:  hmph  20728  hmphtop  20730  hmpher  20736
  Copyright terms: Public domain W3C validator