We extend the unquantified set-theoretic fragment discussed in  with a restricted form of quantification, we prove decidability of the resulting fragment by means of a tableau calculus and we address the efficiency problem of the underlying decision procedure, by showing that the model-checking steps used in  are not necessary.
Cantone, D., & Zarba, C. G. (1999). A tableau-based decision procedure for a fragment of set theory involving a restricted form of quantification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 97–112). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_12