no goals
α : Type u_1
β : Type ?u.66367
γ : Type ?u.66370
ι : Sort u_2
ι' : Sort ?u.66376
f : ι → α
s t : Set α
p : α → Prop
⊢ (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i)
simpa only [exists_prop] using exists_range_iff