As is well-known, the Bernays-Schonfinkel-Ramsey class of all prenex there exists for all V-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are is an element of and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach the remaining part of the decidability result being postponed to a forthcoming paper.