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

Definition df-gic 14967
Description: Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomophic 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  |-  ~=ph𝑔  =  ( `' GrpIso  " ( _V  \  1o ) )

Detailed syntax breakdown of Definition df-gic
StepHypRef Expression
1 cgic 14965 . 2  class  ~=ph𝑔
2 cgim 14964 . . . 4  class GrpIso
32ccnv 4810 . . 3  class  `' GrpIso
4 cvv 2892 . . . 4  class  _V
5 c1o 6646 . . . 4  class  1o
64, 5cdif 3253 . . 3  class  ( _V 
\  1o )
73, 6cima 4814 . 2  class  ( `' GrpIso  " ( _V  \  1o ) )
81, 7wceq 1649 1  wff  ~=ph𝑔  =  ( `' GrpIso  " ( _V  \  1o ) )
Colors of variables: wff set class
This definition is referenced by:  brgic  14976  gicer  14983
  Copyright terms: Public domain W3C validator