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 PID
1 cidom IDomn
2 clpir LPIR
3 1 2 cin ( IDomn ∩ LPIR )
4 0 3 wceq PID = ( IDomn ∩ LPIR )