You can't do this in general, and everywhere, so it's still not rigorous. Consider the embedding of the nats into the reals, where the reals are defined as a subset of the binary sequences (e.g. as the usual infinite binary expansion for (0,1] choosing those that do not terminate in the zeros sequence, but prefix with a Elias-gamma-coded, zigzag-encoded integer). But the usual definition of sequence is as a function from the nats; so are you again going to redefine your reals in terms of that?
In the end you still need to maintain a correspondence between the embedding and the original set as in the typical way where you do that and consider the subset notation as a shorthand that requires you to "lift" or "wrap" through the correspondence wherever necessary.