Metamath Proof Explorer

Theorem hmphi

Description: If there is a homeomorphism between spaces, then the spaces are homeomorphic. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion hmphi 
|- ( F e. ( J Homeo K ) -> J ~= K )

Proof

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 )