case h
α : Type u_2
β : Type u_1
γ : Type ?u.30321
ι : Sort ?u.30324
ι' : Sort ?u.30327
f✝ : α → β
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' ∅ ↔ x✝ ∈ ∅
α : Type u_2
β : Type u_1
γ : Type ?u.30321
ι : Sort ?u.30324
ι' : Sort ?u.30327
f✝ : α → β
s t : Set α
f : α → β
⊢ f '' ∅ = ∅
ext
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.30321
ι : Sort ?u.30324
ι' : Sort ?u.30327
f✝ : α → β
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' ∅ ↔ x✝ ∈ ∅
simp