Description: Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | prmidlssidl | |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmidlidl | |- ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i e. ( LIdeal ` R ) ) |
|
2 | 1 | ex | |- ( R e. Ring -> ( i e. ( PrmIdeal ` R ) -> i e. ( LIdeal ` R ) ) ) |
3 | 2 | ssrdv | |- ( R e. Ring -> ( PrmIdeal ` R ) C_ ( LIdeal ` R ) ) |