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 = { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpir	⊢ LPIR
1		vw	⊢ 𝑤
2		crg	⊢ Ring
3		clidl	⊢ LIdeal
4	1	cv	⊢ 𝑤
5	4 3	cfv	⊢ ( LIdeal ‘ 𝑤 )
6		clpidl	⊢ LPIdeal
7	4 6	cfv	⊢ ( LPIdeal ‘ 𝑤 )
8	5 7	wceq	⊢ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 )
9	8 1 2	crab	⊢ { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }
10	0 9	wceq	⊢ LPIR = { 𝑤 ∈ Ring ∣ ( LIdeal ‘ 𝑤 ) = ( LPIdeal ‘ 𝑤 ) }