Metamath Proof Explorer


Theorem brgic

Description: The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion brgic R 𝑔 S R GrpIso S

Proof

Step Hyp Ref Expression
1 df-gic 𝑔 = GrpIso -1 V 1 𝑜
2 gimfn GrpIso Fn Grp × Grp
3 1 2 brwitnlem R 𝑔 S R GrpIso S