Definition df-pid

Description: Aprincipal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Assertion	df-pid	⊢ PID = ( IDomn ∩ LPIR )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpid	⊢ PID
1		cidom	⊢ IDomn
2		clpir	⊢ LPIR
3	1 2	cin	⊢ ( IDomn ∩ LPIR )
4	0 3	wceq	⊢ PID = ( IDomn ∩ LPIR )