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

Definition df-hmph 20084
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 20082 . 2  class  ~=
2 chmeo 20081 . . . 4  class  Homeo
32ccnv 4998 . . 3  class  `' Homeo
4 cvv 3113 . . . 4  class  _V
5 c1o 7124 . . . 4  class  1o
64, 5cdif 3473 . . 3  class  ( _V 
\  1o )
73, 6cima 5002 . 2  class  ( `'
Homeo " ( _V  \  1o ) )
81, 7wceq 1379 1  wff  ~=  =  ( `' Homeo " ( _V  \  1o ) )
Colors of variables: wff setvar class
This definition is referenced by:  hmph  20104  hmphtop  20106  hmpher  20112
  Copyright terms: Public domain W3C validator