Metamath Proof Explorer


Theorem isomgrrel

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

Ref Expression
Assertion isomgrrel RelIsomGr

Proof

Step Hyp Ref Expression
1 df-isomgr IsomGr=xy|ff:Vtxx1-1 ontoVtxygg:domiEdgx1-1 ontodomiEdgyidomiEdgxfiEdgxi=iEdgygi
2 1 relopabiv RelIsomGr