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 ~=g S <-> ( R GrpIso S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 df-gic 
 |-  ~=g = ( `' GrpIso " ( _V \ 1o ) )
2 gimfn 
 |-  GrpIso Fn ( Grp X. Grp )
3 1 2 brwitnlem 
 |-  ( R ~=g S <-> ( R GrpIso S ) =/= (/) )