Theorem lidlbasel

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

	Ref	Expression
Hypotheses	lidlss.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lidlss.i	⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
Assertion	lidlbasel	⊢ ( ( 𝑈 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lidlss.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		lidlss.i	⊢ 𝐼 = ( LIdeal ‘ 𝑊 )
3	1 2	lidlss	⊢ ( 𝑈 ∈ 𝐼 → 𝑈 ⊆ 𝐵 )
4	3	sselda	⊢ ( ( 𝑈 ∈ 𝐼 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )