no goals
α : Type u_1
β : Type u_2
γ : Type ?u.21814
ι : Sort ?u.21817
ι' : Sort ?u.21820
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
p : β → Prop
⊢ (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
simp