Definition df-lmic

Description: Two modules are said to be isomorphic iff they are connected by at least one isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	df-lmic	⊢ ≃𝑚 = ( ◡ LMIso “ ( V ∖ 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clmic	⊢ ≃𝑚
1		clmim	⊢ LMIso
2	1	ccnv	⊢ ◡ LMIso
3		cvv	⊢ V
4		c1o	⊢ 1o
5	3 4	cdif	⊢ ( V ∖ 1o )
6	2 5	cima	⊢ ( ◡ LMIso “ ( V ∖ 1o ) )
7	0 6	wceq	⊢ ≃𝑚 = ( ◡ LMIso “ ( V ∖ 1o ) )