Definition df-lpir

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpir	|- LPIR
1		vw	|- w
2		crg	|- Ring
3		clidl	|- LIdeal
4	1	cv	|- w
5	4 3	cfv	|- ( LIdeal ` w )
6		clpidl	|- LPIdeal
7	4 6	cfv	|- ( LPIdeal ` w )
8	5 7	wceq	|- ( LIdeal ` w ) = ( LPIdeal ` w )
9	8 1 2	crab	|- { w e. Ring | ( LIdeal ` w ) = ( LPIdeal ` w ) }
10	0 9	wceq	|- LPIR = { w e. Ring | ( LIdeal ` w ) = ( LPIdeal ` w ) }