f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
⊢ y = f z
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
⊢ y = f z
let ⟨w, _, we⟩ := mem_image.1 yx
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
wz : w = z
fy : f w = y
⊢ y = f z
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
⊢ y = f z
let ⟨wz, fy⟩ := pair_injective we
no goals
f : ZFSet → ZFSet
H : Definable 1 f
x z : ZFSet
zx : z ∈ x
y : ZFSet
yx : (fun w => pair z w ∈ map f x) y
w : ZFSet
left✝ : w ∈ x
we : pair w (f w) = pair z y
wz : w = z
fy : f w = y
⊢ y = f z
rw [← fy, wz]