Definition df-gic 17923

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 ∖ 1𝑜))

Detailed syntax breakdown of Definition df-gic

Step	Hyp	Ref	Expression
1		cgic 17921	. 2 class ≃𝑔
2		cgim 17920	. . . 4 class GrpIso
3	2	ccnv 5265	. . 3 class ◡ GrpIso
4		cvv 3340	. . . 4 class V
5		c1o 7723	. . . 4 class 1𝑜
6	4, 5	cdif 3712	. . 3 class (V ∖ 1𝑜)
7	3, 6	cima 5269	. 2 class (◡ GrpIso “ (V ∖ 1𝑜))
8	1, 7	wceq 1632	1 wff ≃𝑔 = (◡ GrpIso “ (V ∖ 1𝑜))

This definition is referenced by:  brgic  17932  gicer  17939