Metamath Proof Explorer

Theorem brgrici

Description: Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025)

Ref Expression
Assertion brgrici 
|- ( F e. ( R GraphIso S ) -> R ~=gr S )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( F e. ( R GraphIso S ) -> ( R GraphIso S ) =/= (/) )
2 brgric 
 |-  ( R ~=gr S <-> ( R GraphIso S ) =/= (/) )
3 1 2 sylibr 
 |-  ( F e. ( R GraphIso S ) -> R ~=gr S )