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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ id x ↔ ∃ z, z ∈ x ∧ y = opair z z
Tactic:
unfold id
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ sep (BoundedFormula.memId (Sum.inr 0) (Sum.inl ())) (fun x_1 => x) (prod x x) ↔ ∃ z, z ∈ x ∧ y = opair z z

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ y ∈ sep (BoundedFormula.memId (Sum.inr 0) (Sum.inl ())) (fun x_1 => x) (prod x x) ↔ ∃ z, z ∈ x ∧ y = opair z z
Tactic:
simp only [mem_sep_iff, interpret_memId']
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ (y ∈ prod x x ∧
      ∃ z,
        z ∈ interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inl ()) ∧
          interpretTerm V (fun x_1 => x) (fun x => y) (Sum.inr 0) = opair z z) ↔
    ∃ z, z ∈ x ∧ y = opair z z

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