Definition df-gic 19181

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	⊢ ≃𝑔 = (◡ GrpIso “ (V ∖ 1o))

Detailed syntax breakdown of Definition df-gic

Step	Hyp	Ref	Expression
1		cgic 19179	. 2 class ≃𝑔
2		cgim 19178	. . . 4 class GrpIso
3	2	ccnv 5666	. . 3 class ◡ GrpIso
4		cvv 3466	. . . 4 class V
5		c1o 8455	. . . 4 class 1o
6	4, 5	cdif 3938	. . 3 class (V ∖ 1o)
7	3, 6	cima 5670	. 2 class (◡ GrpIso “ (V ∖ 1o))
8	1, 7	wceq 1533	1 wff ≃𝑔 = (◡ GrpIso “ (V ∖ 1o))

This definition is referenced by:  brgic  19191  gicer  19198