Description: Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 18-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rnglidl0.u | ||
rnglidl0.z | |||
Assertion | lidl0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rnglidl0.u | ||
2 | rnglidl0.z | ||
3 | ringrng | ||
4 | 1 2 | rnglidl0 | |
5 | 3 4 | syl |