Theorem brgic

Description: The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	brgic	⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-gic	⊢ ≃𝑔 = ( ◡ GrpIso “ ( V ∖ 1o ) )
2		gimfn	⊢ GrpIso Fn ( Grp × Grp )
3	1 2	brwitnlem	⊢ ( 𝑅 ≃𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )