Metamath Proof Explorer

Theorem isomgrsymb

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgrsymb ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → A IsomGr B ↔ B IsomGr A

Proof

Step Hyp Ref Expression
1 isomgrsym ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → A IsomGr B → B IsomGr A
2 isomgrsym ⊢ B ∈ UHGraph ∧ A ∈ UHGraph → B IsomGr A → A IsomGr B
3 2 ancoms ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → B IsomGr A → A IsomGr B
4 1 3 impbid ⊢ A ∈ UHGraph ∧ B ∈ UHGraph → A IsomGr B ↔ B IsomGr A