 The non-sets are usually abandoned (so the formulation of Extensionality is stronger) though ZFA (Zermelo-Fraenkel set theory with atoms) was used in the first independence proofs for the Axiom of Choice.