Metamath Proof Explorer


Theorem isomgrref

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

Ref Expression
Assertion isomgrref GUHGraphGIsomGrG

Proof

Step Hyp Ref Expression
1 id GUHGraphGUHGraph
2 eqid VtxG=VtxG
3 eqid iEdgG=iEdgG
4 2 3 pm3.2i VtxG=VtxGiEdgG=iEdgG
5 4 a1i GUHGraphVtxG=VtxGiEdgG=iEdgG
6 isomgreqve GUHGraphGUHGraphVtxG=VtxGiEdgG=iEdgGGIsomGrG
7 1 1 5 6 syl21anc GUHGraphGIsomGrG