MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pid Structured version   Visualization version   Unicode version
Definition df-pid 19286
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 i^i LPIR )
Detailed syntax breakdown of Definition df-pid
StepHypRef Expression
1 cpid 19282 . 2 class PID
2 cidom 19281 . . 3 class IDomn
3 clpir 19242 . . 3 class LPIR
42, 3cin 3573 . 2 class (IDomn i^i LPIR )
51, 4wceq 1483 1 wff PID = (IDomn i^i LPIR )
Colors of variables: wff setvar class
This definition is referenced by:  ply1pid  23939
  Copyright terms: Public domain W3C validator