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

Definition df-gic 16507
Description: Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
Assertion
Ref Expression
df-gic  |-  ~=g𝑔  =  ( `' GrpIso  " ( _V  \  1o ) )

Detailed syntax breakdown of Definition df-gic
StepHypRef Expression
1 cgic 16505 . 2  class  ~=g𝑔
2 cgim 16504 . . . 4  class GrpIso
32ccnv 4987 . . 3  class  `' GrpIso
4 cvv 3106 . . . 4  class  _V
5 c1o 7115 . . . 4  class  1o
64, 5cdif 3458 . . 3  class  ( _V 
\  1o )
73, 6cima 4991 . 2  class  ( `' GrpIso  " ( _V  \  1o ) )
81, 7wceq 1398 1  wff  ~=g𝑔  =  ( `' GrpIso  " ( _V  \  1o ) )
Colors of variables: wff setvar class
This definition is referenced by:  brgic  16516  gicer  16523
  Copyright terms: Public domain W3C validator