simp only [mem_image_iff, mem_preimage_iff, mem_inverse_iff]
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ y ∈ preimage (inverse r) x ↔ y ∈ image r x
case h
V : Type u_1
inst✝ : Zermelo V
r x y✝ z y : V
⊢ (∃ z, z ∈ x ∧ ∃ y_1 z_1, opair y z = opair y_1 z_1 ∧ opair z_1 y_1 ∈ r) ↔ ∃ z, z ∈ x ∧ opair z y ∈ r