Banach-Tarski paradox states that for a solid ball in 3‑dimensional space, there exists a decomposition into a finite number of disjoint subsets, which can then be put back together in a different way to yield two identical copies of the original one.
Obviously it is based on AC. I was wondering if anyone here knew if analysis under the axioms of ZF has been developed to invent a version of Banach-Tarski which is independent of AC. What the Banach-Tarski paradox looks like without AC? Are there any version of it? (For example one of the theorems that has proved without AC is Heine-Borel theorem.)