x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ ↑x z ↔ ↑y z
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ z ∈ x ↔ z ∈ y
change (x : Class.{u}) z ↔ (y : Class.{u}) z
no goals
x y : ZFSet
h : ↑x = ↑y
z : ZFSet
⊢ ↑x z ↔ ↑y z
rw [h]