simp only [mem_sep_iff, mem_power_iff, interpret_memProd', interpret_inl, ite_true,
  ite_false, interpret_inr, and_iff_right_iff_imp, forall_exists_index, and_imp]
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈
      sep (BoundedFormula.memProd (Sum.inr 0) (Sum.inl true) (Sum.inl false)) (fun i => if i = true then x else y)
        (power (power (x ∪ y))) ↔
    ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ ∀ (x_1 : V), x_1 ∈ x → ∀ (x_2 : V), x_2 ∈ y → z = opair x_1 x_2 → z ⊆ power (x ∪ y)