no goals
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
x : R
⊢ (x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
simp only [iInf, mem_sInf, Set.forall_range_iff]