Theorem: SetTheory.opair_mem_prod_iff (SetTheory/OPair.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z a b : V
⊢ opair a b ∈ prod x y ↔ a ∈ x ∧ b ∈ y
Tactic:
rw [mem_prod_iff]
State after:
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

State before:
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
Tactic:
aesop
State after:
no goals