Metamath Proof Explorer

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 
|- ~=m = ( `' LMIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clmic 
 |-  ~=m
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 
 |-  ~=m = ( `' LMIso " ( _V \ 1o ) )