Theorem: SetTheory.opair_mem_rcomp_iff (SetTheory/Relation.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ opair a c ∈ rcomp s r ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
Tactic:
rw [mem_rcomp_iff]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ (∃ a_1 b c_1, opair a c = opair a_1 c_1 ∧ opair b c_1 ∈ s ∧ opair a_1 b ∈ r) ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a c s : V
⊢ (∃ a_1 b c_1, opair a c = opair a_1 c_1 ∧ opair b c_1 ∈ s ∧ opair a_1 b ∈ r) ↔ ∃ b, opair b c ∈ s ∧ opair a b ∈ r
Tactic:
aesop
State after:
no goals