Metamath Proof Explorer
Description: Definition of the relation x is homeomorphic to y .
(Contributed by FL, 14-Feb-2007)
|
|
Ref |
Expression |
|
Assertion |
df-hmph |
|
Detailed syntax breakdown
Step |
Hyp |
Ref |
Expression |
0 |
|
chmph |
|
1 |
|
chmeo |
|
2 |
1
|
ccnv |
|
3 |
|
cvv |
|
4 |
|
c1o |
|
5 |
3 4
|
cdif |
|
6 |
2 5
|
cima |
|
7 |
0 6
|
wceq |
|