Definition df-gic 19100

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 19098	. 2 class ≃𝑔
2		cgim 19097	. . . 4 class GrpIso
3	2	ccnv 5668	. . 3 class ◡ GrpIso
4		cvv 3473	. . . 4 class V
5		c1o 8441	. . . 4 class 1o
6	4, 5	cdif 3941	. . 3 class (V ∖ 1o)
7	3, 6	cima 5672	. 2 class (◡ GrpIso “ (V ∖ 1o))
8	1, 7	wceq 1541	1 wff ≃𝑔 = (◡ GrpIso “ (V ∖ 1o))

This definition is referenced by:  brgic  19109  gicer  19116