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	|- LNoeR = { a e. Ring | ( ringLMod ` a ) e. LNoeM }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clnr	|- LNoeR
1		va	|- a
2		crg	|- Ring
3		crglmod	|- ringLMod
4	1	cv	|- a
5	4 3	cfv	|- ( ringLMod ` a )
6		clnm	|- LNoeM
7	5 6	wcel	|- ( ringLMod ` a ) e. LNoeM
8	7 1 2	crab	|- { a e. Ring | ( ringLMod ` a ) e. LNoeM }
9	0 8	wceq	|- LNoeR = { a e. Ring | ( ringLMod ` a ) e. LNoeM }