intros a b bmemX bmemY img
α β : 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
α β : Type
X Y : Set α
f : α → β
a : β
b : α
bmemX : b ∈ X
bmemY : b ∈ Y
img : f b = a
⊢ (∃ x ∈ X, f x = a) ∧ ∃ x ∈ Y, f x = a