Metamath Proof Explorer


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 PID = IDomn LPIR

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpid class PID
1 cidom class IDomn
2 clpir class LPIR
3 1 2 cin class IDomn LPIR
4 0 3 wceq wff PID = IDomn LPIR