Metamath Proof Explorer


Theorem islnr

Description: Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion islnr
|- ( A e. LNoeR <-> ( A e. Ring /\ ( ringLMod ` A ) e. LNoeM ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( a = A -> ( ringLMod ` a ) = ( ringLMod ` A ) )
2 1 eleq1d
 |-  ( a = A -> ( ( ringLMod ` a ) e. LNoeM <-> ( ringLMod ` A ) e. LNoeM ) )
3 df-lnr
 |-  LNoeR = { a e. Ring | ( ringLMod ` a ) e. LNoeM }
4 2 3 elrab2
 |-  ( A e. LNoeR <-> ( A e. Ring /\ ( ringLMod ` A ) e. LNoeM ) )