This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in Ring \to PrmIdeal (R) \subseteq LIdeal (R)$

Step	Hyp	Ref	Expression
1		prmidlidl	$⊢ (R \in Ring \land i \in PrmIdeal (R)) \to i \in LIdeal (R)$
2	1	ex	$⊢ R \in Ring \to (i \in PrmIdeal (R) \to i \in LIdeal (R))$
3	2	ssrdv	$⊢ R \in Ring \to PrmIdeal (R) \subseteq LIdeal (R)$