case a
z : ZFSet
⊢ congToClass ∅ z ↔ ∅ z
⊢ congToClass ∅ = ∅
ext z
case a
z : ZFSet
⊢ ¬setOf (fun y => ↑y ∈ ∅) z
case a
z : ZFSet
⊢ congToClass ∅ z ↔ ∅ z
simp only [congToClass, not_empty_hom, iff_false_iff]
no goals
case a
z : ZFSet
⊢ ¬setOf (fun y => ↑y ∈ ∅) z
exact Set.not_mem_empty z