no goals
α : Type u_1
β : Type ?u.128718
γ : Type ?u.128721
ι : Sort ?u.128724
ι' : Sort ?u.128727
ι₂ : Sort ?u.128730
κ : ι → Sort ?u.128735
κ₁ : ι → Sort ?u.128740
κ₂ : ι → Sort ?u.128745
κ' : ι' → Sort ?u.128750
c : Set (Set α)
⊢ ⋃₀ c = univ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ a ∈ b
simp only [eq_univ_iff_forall, mem_sUnion]