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	$$⊢B={\mathrm{Base}}_W$$
	lidlss.i	$$⊢I=\mathrm{LIdeal}\left(W\right)$$
Assertion	lidlbasel	$$⊢\left(U\in I\wedge X\in U\right)\to X\in B$$

Proof

Step	Hyp	Ref	Expression
1		lidlss.b	$$⊢B={\mathrm{Base}}_W$$
2		lidlss.i	$$⊢I=\mathrm{LIdeal}\left(W\right)$$
3	1 2	lidlss	$$⊢U\in I\to U\subseteq B$$
4	3	sselda	$$⊢\left(U\in I\wedge X\in U\right)\to X\in B$$