α : Type u_2
β : Type u_1
γ : Type ?u.75177
ι : Sort ?u.75180
ι' : Sort ?u.75183
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
α : Type u_2
β : Type u_1
γ : Type ?u.75177
ι : Sort ?u.75180
ι' : Sort ?u.75183
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)
rw [← exists_range_iff, range_image]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.75177
ι : Sort ?u.75180
ι' : Sort ?u.75183
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
rfl