I doubt that there is any generally accepted definition of "structured set" in mathematics that includes a notion of morphism and does not already use the technology of category theory. (For a "behavioral" definition that does use category theory, see for instance here.) As has been noted in the comments, very few mathematicians have even ever seen Bourbaki's actual definition, and it probably had some issues.
The definition you propose seems too broad. Allowing arbitrary formulas of set theory enables axioms like "$x=\{\emptyset\}$", so you would have a type of structure such that $\{\emptyset\}$ admits that structure but $\{\{\emptyset\}\}$ does not. This is contrary to the general understanding of structuralism that a "structure" should be transportable across any bijection.
Probably the best-known general notion of "structured set" that forms a category (and is isomorphism-invariant) would be the models of a first-order theory. One can expand the class of models here by considering infinitary languages. However, this doesn't include examples such as topological spaces, which are still intuitively "structured sets".
The obvious way to remedy this difficulty is to use higher-order logic. The problem is that there is no obvious "correct" way to define non-invertible morphisms between models of a higher-order theory. How do you make continuous maps of topological spaces fall out of a general notion of morphism, given the contravariant character of continuity on open sets?
There are at least partial solutions to this problem, although I don't think any of them is standard or well-known. For instance, the double powerset functor is covariantly functorial in a canonical way (induced from the contravariant functoriality of the single powerset), so if we restrict our higher-order signatures to contain only relations between elements of iterated powersets $P^n(x)$ where $n$ is even, then there is a straightforward definition of morphism of structures. One can then represent and axiomatize topological spaces with such a signature having a single predicate on $P(P(x))$ that picks out the supersets of the topology, and the induced morphisms will be continuous maps. (We discovered this as part of our work on the higher structure identity principle.)
It's less clear that this approach can also represent morphisms between structures that should be covariant on subsets, but it seems to to be possible in at least some cases, such as suplattices. One could also try to augment a higher-order signature with explicit "variance information" that would determine the morphisms. Unfortunately, it's hard to make (let alone prove) a general claim that any such approach "always works" without any existing general notion of "structure" (with attendant notion of morphism) to compare it to!
Defining invertible morphisms between structures, on the other hand, is entirely straightforward. So if all you want is a groupoid of structures, then higher-order logic should do the job. This is one of the arguments for the "more foundational" nature of groupoids over categories: the groupoid of topological spaces (for instance) is uniquely and canonically determined by the notion of "topological space" (expressed, for instance, as a higher-order theory), but the same can't really be said for the usual category of topological spaces (from a purely abstract point of view, what privileges continuous maps over, say, open maps?).
So if your goal is just to have a definition with which to "speak about mathematical structures as the main subject of study of mathematics", I would say that higher-order logic is probably the best answer. If you also want to use this as a lead-in to introduce category theory, then my suggestion would probably be to discuss particular examples, then general morphisms of models of first-order theories, then isomorphisms of models of higher-order theories, then mention that defining a correct general notion of noninvertible morphism in terms of a higher-order theory is tricky, and finally use that difficulty as a motivation to refocus attention not on the notion of structure (i.e. the objects of the category) but on the entire category itself as an object of study.
