Database
BASIC TOPOLOGY
Topology
Homeomorphisms
hmphsymb
Next ⟩
haushmphlem
Metamath Proof Explorer
Ascii
Unicode
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