Theorem: SetTheory.mem_apply_iff (SetTheory/Function.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ apply f x ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
Tactic:
unfold apply
State after:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ ⋃ image f {x} ↔ ∃ z, opair x z ∈ f ∧ y ∈ z

State before:
V : Type u_1
inst✝ : Zermelo V
r x y z a b c f : V
⊢ y ∈ ⋃ image f {x} ↔ ∃ z, opair x z ∈ f ∧ y ∈ z
Tactic:
simp [mem_image_iff]
State after:
no goals