Definition df-pid 21641

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

Assertion

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

Detailed syntax breakdown of Definition df-pid

Step	Hyp	Ref	Expression
1		cpid 21640	. 2 class PID
2		cidom 20925	. . 3 class IDomn
3		clpir 21625	. . 3 class LPIR
4	2, 3	cin 3898	. 2 class (IDomn ∩ LPIR)
5	1, 4	wceq 1570	1 wff PID = (IDomn ∩ LPIR)

This definition is used by:  ply1pid  26481  mxidlirred  33979  rprmirredb  34046  pidufd  34057  zringpid  34066