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

Definition df-pid 19980
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
StepHypRef Expression
1 cpid 19976 . 2 class PID
2 cidom 19975 . . 3 class IDomn
3 clpir 19936 . . 3 class LPIR
42, 3cin 3938 . 2 class (IDomn ∩ LPIR)
51, 4wceq 1530 1 wff PID = (IDomn ∩ LPIR)
Colors of variables: wff setvar class
This definition is referenced by:  ply1pid  24688
  Copyright terms: Public domain W3C validator