Metamath Proof Explorer

Theorem gricsymb

Description: Graph isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 11-Nov-2022) (Proof shortened by AV, 3-May-2025)

Ref Expression
Assertion gricsymb 
|- ( ( A e. UHGraph /\ B e. UHGraph ) -> ( A ~=gr B <-> B ~=gr A ) )

Proof

Step Hyp Ref Expression
1 gricsym 
 |-  ( A e. UHGraph -> ( A ~=gr B -> B ~=gr A ) )
2 gricsym 
 |-  ( B e. UHGraph -> ( B ~=gr A -> A ~=gr B ) )
3 1 2 anbiim 
 |-  ( ( A e. UHGraph /\ B e. UHGraph ) -> ( A ~=gr B <-> B ~=gr A ) )