Theorem srhmsubclem1

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

	Ref	Expression
Hypotheses	srhmsubc.s	|- A. r e. S r e. Ring
	srhmsubc.c	|- C = ( U i^i S )
Assertion	srhmsubclem1	|- ( X e. C -> X e. ( U i^i Ring ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	|- A. r e. S r e. Ring
2		srhmsubc.c	|- C = ( U i^i S )
3		eleq1	|- ( r = X -> ( r e. Ring <-> X e. Ring ) )
4	3 1	vtoclri	|- ( X e. S -> X e. Ring )
5	4	anim2i	|- ( ( X e. U /\ X e. S ) -> ( X e. U /\ X e. Ring ) )
6	2	elin2	|- ( X e. C <-> ( X e. U /\ X e. S ) )
7		elin	|- ( X e. ( U i^i Ring ) <-> ( X e. U /\ X e. Ring ) )
8	5 6 7	3imtr4i	|- ( X e. C -> X e. ( U i^i Ring ) )