case h
α : Type u_2
β : Type u_1
γ : Type ?u.36244
ι : Sort ?u.36247
ι' : Sort ?u.36250
f✝ : α → β
s t : Set α
f : α → β
a : α
x✝ : β
⊢ x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}
α : Type u_2
β : Type u_1
γ : Type ?u.36244
ι : Sort ?u.36247
ι' : Sort ?u.36250
f✝ : α → β
s t : Set α
f : α → β
a : α
⊢ f '' {a} = {f a}
ext
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.36244
ι : Sort ?u.36247
ι' : Sort ?u.36250
f✝ : α → β
s t : Set α
f : α → β
a : α
x✝ : β
⊢ x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}
simp [image, eq_comm]