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

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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memDom (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair x z ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memDom', interpret_inr, interpret_inl,
  and_iff_right_iff_imp, forall_exists_index]
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x x_1 ∈ r → x ∈ ⋃ ⋃ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ ∀ (x_1 : V), opair x x_1 ∈ r → x ∈ ⋃ ⋃ r
Tactic:
intro t
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair x t ∈ r → x ∈ ⋃ ⋃ r

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z t : V
⊢ opair x t ∈ r → x ∈ ⋃ ⋃ r
Tactic:
exact opair_left_mem_sUnion_sUnion
State after:
no goals