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	$$⊢\mathrm{PID}=\mathrm{IDomn}\cap \mathrm{LPIR}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpid	$$class\mathrm{PID}$$
1		cidom	$$class\mathrm{IDomn}$$
2		clpir	$$class\mathrm{LPIR}$$
3	1 2	cin	$$class\left(\mathrm{IDomn}\cap \mathrm{LPIR}\right)$$
4	0 3	wceq	$$wff\mathrm{PID}=\mathrm{IDomn}\cap \mathrm{LPIR}$$