Metamath Proof Explorer

Theorem grlicsymb

Description: Graph local isomorphism is symmetric in both directions for hypergraphs. (Contributed by AV, 9-Jun-2025)

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

Proof

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