constructor
case h
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y ↔ ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1
case h.mp
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ z ∈ y → ∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1

case h.mpr
V : Type u_1
inst✝ : Zermelo V
r x y z✝ a b c : V
f : a ⟶ b
h : opair x y ∈ f.graph
z : V
⊢ (∃ z_1, opair x z_1 ∈ f.graph ∧ z ∈ z_1) → z ∈ y