Metamath Proof Explorer

Theorem prmidlssidl

Description: Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024)

Ref Expression
Assertion prmidlssidl ⊢ R ∈ Ring → PrmIdeal ⁡ R ⊆ LIdeal ⁡ R

Proof

Step Hyp Ref Expression
1 prmidlidl ⊢ R ∈ Ring ∧ i ∈ PrmIdeal ⁡ R → i ∈ LIdeal ⁡ R
2 1 ex ⊢ R ∈ Ring → i ∈ PrmIdeal ⁡ R → i ∈ LIdeal ⁡ R
3 2 ssrdv ⊢ R ∈ Ring → PrmIdeal ⁡ R ⊆ LIdeal ⁡ R