Metamath Proof Explorer

Definition df-hmph

Description: Definition of the relation x is homeomorphic to y . (Contributed by FL, 14-Feb-2007)

Ref Expression
Assertion df-hmph 
|- ~= = ( `' Homeo " ( _V \ 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 chmph 
 |-  ~=
1 chmeo 
 |-  Homeo
2 1 ccnv 
 |-  `' Homeo
3 cvv 
 |-  _V
4 c1o 
 |-  1o
5 3 4 cdif 
 |-  ( _V \ 1o )
6 2 5 cima 
 |-  ( `' Homeo " ( _V \ 1o ) )
7 0 6 wceq 
 |-  ~= = ( `' Homeo " ( _V \ 1o ) )