Proofs in Classical Set Theory using logical set membership conditions Main Question: When proving theorems about sets (at the level of rigor which one would when studying introductory algebra), its common to translate between functions of sets and the logic of set membership, i.e.
$$
A-B\quad \text{has the membership condition}\quad x\in A \wedge x\notin B
$$
So, consider if one wanted to prove that the symmetric difference $A*B:=(A-B)\cup(B-A)$ could also be expressed as $(A\cup B) - (A\cap B)$. Would it be considered good practice to show that the membership condition of the former,
$$
(A-B)\cup(B-A)\quad\equiv\quad(x\in A \wedge x\notin B) \vee(x\in B \wedge x\notin A)
$$
is logically equivalent (by rules of logical inference/simplification) to the membership condition of the latter,
$$
(A\cup B) - (A\cap B)\quad\equiv\quad(x\in A\vee x\in B)\wedge\neg(x\in A \wedge x\in B)
$$
More importantly, would it be sufficient to prove the result after establishing the logical equivalence?
Optionally: (if the above answer is in the affimative) At a higher level of abstraction, is there a high-level symmetry between the class of sets and the class of set membership conditions (i.e. logical statements) that explain why one representation can be exchanged for another at no cost to the soundness of the inference?
Thanks for reading and considering the question.
 A: In ZFC, probably the most commonly used rigorous set theory, this is an axiom, called the axiom of extensionality. It states that for every pair of sets $x, y$, we have $x = y$ iff $x$ and $y$ have the same members. That is, $(\forall x)(\forall y)(x = y \iff (\forall z)(z \in x \iff z \in y))$.
That is, we declare it to be true that if two sets are defined by the same membership property, then they are the same set.
But do note that it's not always true that a membership property does define a set. The standard example is the membership property "true", which always holds; but there is no set of all sets (see Russell's paradox). You can only define a set via a membership property if you're using the property to select a subset of a set that is known already to exist. (The axiom [schema] which states that you can do this is known by several names, such as the axiom schema of specification.) In your example, $A \cup B$ is a sufficient set to be selecting a subset of, so it's justified.

Note that the axiom of extensionality is really saying something. One could imagine an "intensional" world where "sets" were defined in a more fine-grained way, so that $\{2n+1 : n \in \mathbb{N}\}$ were different to $\{2n - 1 : n \in \mathbb{N} \setminus\{0\}\}$ by virtue of their different descriptions. This example is pretty trivial, but it becomes a bit more compelling when applied to functions: why should $n \mapsto 2n$ be the same as the function $n \mapsto n+n$, since they're manifestly computed in a different way? But we define sets to be a type of collection which doesn't care about this kind of difference.
