no goals
α : Type u_1
β : Type ?u.166966
γ : Type ?u.166969
ι : Sort ?u.166972
ι' : Sort ?u.166975
ι₂ : Sort ?u.166978
κ : ι → Sort ?u.166983
κ₁ : ι → Sort ?u.166988
κ₂ : ι → Sort ?u.166993
κ' : ι' → Sort ?u.166998
s : Set (Set α)
⊢ ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i
rw [← sUnion_image, image_id']