unfold prod
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ prod x y ↔ ∃ a, a ∈ x ∧ ∃ b, b ∈ y ∧ z = opair a b
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