case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (insert x y) ↔ x✝ ∈ insert x (toSet y)
x y : ZFSet
⊢ toSet (insert x y) = insert x (toSet y)
ext
no goals
case h
x y x✝ : ZFSet
⊢ x✝ ∈ toSet (insert x y) ↔ x✝ ∈ insert x (toSet y)
simp