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

Definition df-hmph 21780
Description: Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.)
Assertion
Ref Expression
df-hmph ≃ = (Homeo “ (V ∖ 1𝑜))

Detailed syntax breakdown of Definition df-hmph
StepHypRef Expression
1 chmph 21778 . 2 class
2 chmeo 21777 . . . 4 class Homeo
32ccnv 5249 . . 3 class Homeo
4 cvv 3351 . . . 4 class V
5 c1o 7710 . . . 4 class 1𝑜
64, 5cdif 3720 . . 3 class (V ∖ 1𝑜)
73, 6cima 5253 . 2 class (Homeo “ (V ∖ 1𝑜))
81, 7wceq 1631 1 wff ≃ = (Homeo “ (V ∖ 1𝑜))
Colors of variables: wff setvar class
This definition is referenced by:  hmph  21800  hmphtop  21802  hmpher  21808
  Copyright terms: Public domain W3C validator