unfold image
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ image r y ↔ ∃ z, z ∈ y ∧ opair z x ∈ r
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memImage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (ran r) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r