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

Metamath Proof Explorer

Theorem idlcl

Description: An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	idlss.1	$⊢ G = 1^{st} (R)$
	idlss.2	$⊢ X = ran G$
Assertion	idlcl	$⊢ ((R \in RingOps \land I \in Idl (R)) \land A \in I) \to A \in X$

Step	Hyp	Ref	Expression
1		idlss.1	$⊢ G = 1^{st} (R)$
2		idlss.2	$⊢ X = ran G$
3	1 2	idlss	$⊢ (R \in RingOps \land I \in Idl (R)) \to I \subseteq X$
4	3	sselda	$⊢ ((R \in RingOps \land I \in Idl (R)) \land A \in I) \to A \in X$