simp [Set.subset_def]
α β : Type
X Y : Set α
f : α → β
⊢ ∀ x ∈ f '' (X ∩ Y), x ∈ f '' X ∩ f '' Y
α β : Type
X Y : Set α
f : α → β
⊢ ∀ (x : β), ∀ x_1 ∈ X, x_1 ∈ Y → f x_1 = x → (∃ x_2 ∈ X, f x_2 = x) ∧ ∃ x_2 ∈ Y, f x_2 = x