simp only [mem_sep_iff, mem_ran_iff, interpret_memImage']
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
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair z x ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair z (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair z x ∈ r