Metamath Proof Explorer

Theorem brgric

Description: The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025)

Ref Expression
Assertion brgric 
|- ( R ~=gr S <-> ( R GraphIso S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-gric 
 |-  ~=gr = ( `' GraphIso " ( _V \ 1o ) )
2 grimfn 
 |-  GraphIso Fn ( _V X. _V )
3 1 2 brwitnlem 
 |-  ( R ~=gr S <-> ( R GraphIso S ) =/= (/) )