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

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

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z : V
⊢ x ∈ sep (BoundedFormula.memRan (Sum.inr 0) (Sum.inl ())) (fun x => r) (⋃ ⋃ r) ↔ ∃ z, opair z x ∈ r
Tactic:
simp only [mem_sep_iff, interpret_memRan', 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_1 x ∈ r → x ∈ ⋃ ⋃ r

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

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