Metamath Proof Explorer

Theorem isomgrsymb

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

Ref Expression
Assertion isomgrsymb 
|- ( ( A e. UHGraph /\ B e. UHGraph ) -> ( A IsomGr B <-> B IsomGr A ) )

Proof

Step Hyp Ref Expression
1 isomgrsym 
 |-  ( ( A e. UHGraph /\ B e. UHGraph ) -> ( A IsomGr B -> B IsomGr A ) )
2 isomgrsym 
 |-  ( ( B e. UHGraph /\ A e. UHGraph ) -> ( B IsomGr A -> A IsomGr B ) )
3 2 ancoms 
 |-  ( ( A e. UHGraph /\ B e. UHGraph ) -> ( B IsomGr A -> A IsomGr B ) )
4 1 3 impbid 
 |-  ( ( A e. UHGraph /\ B e. UHGraph ) -> ( A IsomGr B <-> B IsomGr A ) )