Theorem srhmsubclem1

Description: Lemma 1 for srhmsubc . (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
	srhmsubc.c	$$⊢C=U\cap S$$
Assertion	srhmsubclem1	$$⊢X\in C\to X\in \left(U\cap \mathrm{Ring}\right)$$

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	$$⊢\forall r\in Sr\in \mathrm{Ring}$$
2		srhmsubc.c	$$⊢C=U\cap S$$
3		eleq1	$$⊢r=X\to \left(r\in \mathrm{Ring}\leftrightarrow X\in \mathrm{Ring}\right)$$
4	3 1	vtoclri	$$⊢X\in S\to X\in \mathrm{Ring}$$
5	4	anim2i	$$⊢\left(X\in U\wedge X\in S\right)\to \left(X\in U\wedge X\in \mathrm{Ring}\right)$$
6	2	elin2	$$⊢X\in C\leftrightarrow \left(X\in U\wedge X\in S\right)$$
7		elin	$$⊢X\in \left(U\cap \mathrm{Ring}\right)\leftrightarrow \left(X\in U\wedge X\in \mathrm{Ring}\right)$$
8	5 6 7	3imtr4i	$$⊢X\in C\to X\in \left(U\cap \mathrm{Ring}\right)$$