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	$$⊢\mathrm{LPIR}=\left\{w\in \mathrm{Ring}|\mathrm{LIdeal}\left(w\right)=\mathrm{LPIdeal}\left(w\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpir	$$class\mathrm{LPIR}$$
1		vw	$$setvarw$$
2		crg	$$class\mathrm{Ring}$$
3		clidl	$$class\mathrm{LIdeal}$$
4	1	cv	$$setvarw$$
5	4 3	cfv	$$class\mathrm{LIdeal}\left(w\right)$$
6		clpidl	$$class\mathrm{LPIdeal}$$
7	4 6	cfv	$$class\mathrm{LPIdeal}\left(w\right)$$
8	5 7	wceq	$$wff\mathrm{LIdeal}\left(w\right)=\mathrm{LPIdeal}\left(w\right)$$
9	8 1 2	crab	$$class\left\{w\in \mathrm{Ring}|\mathrm{LIdeal}\left(w\right)=\mathrm{LPIdeal}\left(w\right)\right\}$$
10	0 9	wceq	$$wff\mathrm{LPIR}=\left\{w\in \mathrm{Ring}|\mathrm{LIdeal}\left(w\right)=\mathrm{LPIdeal}\left(w\right)\right\}$$