Definition df-lnr

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

	Ref	Expression
Assertion	df-lnr	$$⊢\mathrm{LNoeR}=\left\{a\in \mathrm{Ring}|\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clnr	$$class\mathrm{LNoeR}$$
1		va	$$setvara$$
2		crg	$$class\mathrm{Ring}$$
3		crglmod	$$class\mathrm{ringLMod}$$
4	1	cv	$$setvara$$
5	4 3	cfv	$$class\mathrm{ringLMod}\left(a\right)$$
6		clnm	$$class\mathrm{LNoeM}$$
7	5 6	wcel	$$wff\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}$$
8	7 1 2	crab	$$class\left\{a\in \mathrm{Ring}|\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}\right\}$$
9	0 8	wceq	$$wff\mathrm{LNoeR}=\left\{a\in \mathrm{Ring}|\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}\right\}$$