α✝ : Type ?u.37986
β✝ : Type ?u.37989
γ : Type ?u.37992
ι : Sort ?u.37995
ι' : Sort ?u.37998
f✝ : α✝ → β✝
s✝ t : Set α✝
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s
α✝ : Type ?u.37986
β✝ : Type ?u.37989
γ : Type ?u.37992
ι : Sort ?u.37995
ι' : Sort ?u.37998
f✝ : α✝ → β✝
s✝ t : Set α✝
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅
simp only [eq_empty_iff_forall_not_mem]
no goals
α✝ : Type ?u.37986
β✝ : Type ?u.37989
γ : Type ?u.37992
ι : Sort ?u.37995
ι' : Sort ?u.37998
f✝ : α✝ → β✝
s✝ t : Set α✝
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s
exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩