Description: Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lpival.p | |
|
lpiss.u | |
||
Assertion | islpir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lpival.p | |
|
2 | lpiss.u | |
|
3 | fveq2 | |
|
4 | fveq2 | |
|
5 | 3 4 | eqeq12d | |
6 | 2 1 | eqeq12i | |
7 | 5 6 | bitr4di | |
8 | df-lpir | |
|
9 | 7 8 | elrab2 | |