Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gim Structured version   Unicode version

Definition df-gim 15038
 Description: An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.)
Assertion
Ref Expression
df-gim GrpIso
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-gim
StepHypRef Expression
1 cgim 15036 . 2 GrpIso
2 vs . . 3
3 vt . . 3
4 cgrp 14677 . . 3
52cv 1651 . . . . . 6
6 cbs 13461 . . . . . 6
75, 6cfv 5446 . . . . 5
83cv 1651 . . . . . 6
98, 6cfv 5446 . . . . 5
10 vg . . . . . 6
1110cv 1651 . . . . 5
127, 9, 11wf1o 5445 . . . 4
13 cghm 14995 . . . . 5
145, 8, 13co 6073 . . . 4
1512, 10, 14crab 2701 . . 3
162, 3, 4, 4, 15cmpt2 6075 . 2
171, 16wceq 1652 1 GrpIso
 Colors of variables: wff set class This definition is referenced by:  gimfn  15040  isgim  15041
 Copyright terms: Public domain W3C validator