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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ preimage r y ↔ ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
unfold preimage
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memPreimage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (dom r) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈
      sep (BoundedFormula.memPreimage (Sum.inr 0) (Sum.inl false) (Sum.inl true)) (fun i => if i = true then r else y)
        (dom r) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
simp only [mem_sep_iff, mem_dom_iff, interpret_memPreimage']
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair x z ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) z ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ((∃ z, opair x z ∈ r) ∧
      ∃ z,
        z ∈ interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl false) ∧
          opair (interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inr 0)) z ∈
            interpretTerm V (fun i => if i = true then r else y) (fun x_1 => x) (Sum.inl true)) ↔
    ∃ z, z ∈ y ∧ opair x z ∈ r
Tactic:
aesop
State after:
no goals