rw [mem_prod_iff]
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ opair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ (∃ a_1, a_1 ∈ x ∧ ∃ b_1, b_1 ∈ y ∧ opair a b = opair a_1 b_1) ↔ a ∈ x ∧ b ∈ y