Metamath Proof Explorer


Theorem hmphsymb

Description: "Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007)

Ref Expression
Assertion hmphsymb ⊢ J ≃ K ↔ K ≃ J

Proof

Step Hyp Ref Expression
1 hmphsym ⊢ J ≃ K → K ≃ J
2 hmphsym ⊢ K ≃ J → J ≃ K
3 1 2 impbii ⊢ J ≃ K ↔ K ≃ J