Description: If there is a homeomorphism between spaces, then the spaces are homeomorphic. (Contributed by Mario Carneiro, 23Aug2015)
Ref  Expression  

Assertion  hmphi   ( F e. ( J Homeo K ) > J ~= K ) 
Step  Hyp  Ref  Expression 

1  ne0i   ( F e. ( J Homeo K ) > ( J Homeo K ) =/= (/) ) 

2  hmph   ( J ~= K <> ( J Homeo K ) =/= (/) ) 

3  1 2  sylibr   ( F e. ( J Homeo K ) > J ~= K ) 