Definition df-gic 19524

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 19522	. 2 class ≃𝑔
2		cgim 19521	. . . 4 class GrpIso
3	2	ccnv 5657	. . 3 class ◡ GrpIso
4		cvv 3454	. . . 4 class V
5		c1o 8507	. . . 4 class 1o
6	4, 5	cdif 4048	. . 3 class (V ∖ 1o)
7	3, 6	cima 5661	. 2 class (◡ GrpIso “ (V ∖ 1o))
8	1, 7	wceq 1570	1 wff ≃𝑔 = (◡ GrpIso “ (V ∖ 1o))

This definition is used by:  brgic  19535  gicer  19542