α : Type u_2
β : Type u_1
γ : Type ?u.76965
ι : Sort ?u.76968
ι' : Sort ?u.76971
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
α : Type u_2
β : Type u_1
γ : Type ?u.76965
ι : Sort ?u.76968
ι' : Sort ?u.76971
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (s : Set α), p (f '' s)
rw [← forall_range_iff, range_image]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.76965
ι : Sort ?u.76968
ι' : Sort ?u.76971
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
rfl