no goals
α : Type u_2
β : Type u_1
γ : Type ?u.89300
inst✝ : DecidableEq β
f✝ g : α → β
s : Finset α
t : Finset β
a✝ : α
b c : β
f : α → β
a : α
x : β
⊢ x ∈ image f {a} ↔ x ∈ {f a}
simpa only [mem_image, exists_prop, mem_singleton, exists_eq_left] using eq_comm