Theorem srhmsubclem1

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

	Ref	Expression
Hypotheses	srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
	srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
Assertion	srhmsubclem1	⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( 𝑈 ∩ Ring ) )

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	⊢ ∀ 𝑟 ∈ 𝑆 𝑟 ∈ Ring
2		srhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ 𝑆 )
3		eleq1	⊢ ( 𝑟 = 𝑋 → ( 𝑟 ∈ Ring ↔ 𝑋 ∈ Ring ) )
4	3 1	vtoclri	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ Ring )
5	4	anim2i	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ Ring ) )
6	2	elin2	⊢ ( 𝑋 ∈ 𝐶 ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ 𝑆 ) )
7		elin	⊢ ( 𝑋 ∈ ( 𝑈 ∩ Ring ) ↔ ( 𝑋 ∈ 𝑈 ∧ 𝑋 ∈ Ring ) )
8	5 6 7	3imtr4i	⊢ ( 𝑋 ∈ 𝐶 → 𝑋 ∈ ( 𝑈 ∩ Ring ) )