mathlib3

16478385 - feat(set_theory/zfc/basic): `pSet` with empty type is equivalent to `Ø` (#15550)

feat(set_theory/zfc/basic): `pSet` with empty type is equivalent to `Ø` (#15550) We also add `Set.equiv_iff`, which unfolds the definition of `equiv` in terms of `Set.func` and `Set.type`.