df-pid - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-pid		Structured version Visualization version GIF version

Definition df-pid 20062

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 20058	. 2 class PID
2		cidom 20057	. . 3 class IDomn
3		clpir 20018	. . 3 class LPIR
4	2, 3	cin 3938	. 2 class (IDomn ∩ LPIR)
5	1, 4	wceq 1536	1 wff PID = (IDomn ∩ LPIR)

Colors of variables: wff setvar class

This definition is referenced by: ply1pid 24776

W3C validator