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 ) )