Definition df-lnr 39708

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 39707	. 2 class LNoeR
2		va	. . . . . 6 setvar 𝑎
3	2	cv 1532	. . . . 5 class 𝑎
4		crglmod 19940	. . . . 5 class ringLMod
5	3, 4	cfv 6354	. . . 4 class (ringLMod‘𝑎)
6		clnm 39673	. . . 4 class LNoeM
7	5, 6	wcel 2110	. . 3 wff (ringLMod‘𝑎) ∈ LNoeM
8		crg 19296	. . 3 class Ring
9	7, 2, 8	crab 3142	. 2 class {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}
10	1, 9	wceq 1533	1 wff LNoeR = {𝑎 ∈ Ring ∣ (ringLMod‘𝑎) ∈ LNoeM}

This definition is referenced by:  islnr  39709