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 = ( 1st ` R )
	idlss.2	|- X = ran G
Assertion	idlcl	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> A e. X )

Proof

Step	Hyp	Ref	Expression
1		idlss.1	|- G = ( 1st ` R )
2		idlss.2	|- X = ran G
3	1 2	idlss	|- ( ( R e. RingOps /\ I e. ( Idl ` R ) ) -> I C_ X )
4	3	sselda	|- ( ( ( R e. RingOps /\ I e. ( Idl ` R ) ) /\ A e. I ) -> A e. X )