Definition df-lpir 19244

Description: Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)

Assertion

Ref	Expression
df-lpir	|- LPIR = { w e. Ring | (LIdeal ` w ) = (LPIdeal ` w ) }

Detailed syntax breakdown of Definition df-lpir

Step	Hyp	Ref	Expression
1		clpir 19242	. 2 class LPIR
2		vw	. . . . . 6 setvar w
3	2	cv 1482	. . . . 5 class w
4		clidl 19170	. . . . 5 class LIdeal
5	3, 4	cfv 5888	. . . 4 class (LIdeal ` w )
6		clpidl 19241	. . . . 5 class LPIdeal
7	3, 6	cfv 5888	. . . 4 class (LPIdeal ` w )
8	5, 7	wceq 1483	. . 3 wff (LIdeal ` w ) = (LPIdeal ` w )
9		crg 18547	. . 3 class Ring
10	8, 2, 9	crab 2916	. 2 class { w e. Ring | (LIdeal ` w ) = (LPIdeal ` w ) }
11	1, 10	wceq 1483	1 wff LPIR = { w e. Ring | (LIdeal ` w ) = (LPIdeal ` w ) }

This definition is referenced by:  islpir  19249