Definition df-lnr 40935

Description: A ring is left-Noetherian iff it is Noetherian as a left module over itself. (Contributed by Stefan O'Rear, 24-Jan-2015.)

Assertion

Ref	Expression
df-lnr	⊢ LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

Detailed syntax breakdown of Definition df-lnr

Step	Hyp	Ref	Expression
1		clnr 40934	. 2 class LNoeR
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1538	. . . . 5 class 𝑎
4		crglmod 20431	. . . . 5 class ringLMod
5	3, 4	cfv 6433	. . . 4 class (ringLMod‘𝑎)
6		clnm 40900	. . . 4 class LNoeM
7	5, 6	wcel 2106	. . 3 wff (ringLMod‘𝑎) ∈ LNoeM
8		crg 19783	. . 3 class Ring
9	7, 2, 8	crab 3068	. 2 class {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}
10	1, 9	wceq 1539	1 wff LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

This definition is referenced by:  islnr  40936