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 -1 V 1 𝑜

Detailed syntax breakdown

Step Hyp Ref Expression
0 chmph class
1 chmeo class Homeo
2 1 ccnv class Homeo -1
3 cvv class V
4 c1o class 1 𝑜
5 3 4 cdif class V 1 𝑜
6 2 5 cima class Homeo -1 V 1 𝑜
7 0 6 wceq wff = Homeo -1 V 1 𝑜