Prove distributive law of sets
Your proof of the one direction looks perfectly fine. It is very common to use "and" and "or" written in a meta-level proof. However, if you feel this getting into the way of displaying an argument, you may benefit by some more formalism, e.g.
\begin{align}x\in A\cap(B\cup C) &\Rightarrow x\in A\land x\in (B\cup C)\\ &\Rightarrow x\in A\land (x\in B\lor x\in C)\\&\Rightarrow (x\in A\land x\in B)\lor (x\in A\land x\in C)\\&\Rightarrow x\in A\cap B\lor x\in A\cap C\\ &\Rightarrow x\in(A\cap B)\cup (A\cap C)\end{align}
I'm using $\land,\lor$ here as symbols of the "and","or" respectively.
I this specific case, the proof relies on using the distributive property of $\land,\lor$ as logical connectives to prove the corresponding property of unions and intersections via set membership. (this connection of course comes as no surprise through the common connection to boolean algebra(s)).
So, having this translation of very similar connectives/operations into one another as the essence of a proof can seems a little ambiguous, although it is the heart of the argument.
In general, I think the key to a clear exposition of course always depends on the context, but it is almost always a good mix of formatting, formalism and non-formalism.
E.g. no one wants to write precise first-order set theory statements for every mathematical concept, although it would be formally strict. In cases like the above, or in general with chains of implications or bi-implications, a structured formatting of the steps, like the aligned presentation above, can already improve the exposition a lot.
EDIT: Note, that you can turn every implication in the above chain into a bi-implication, i.e. by the argument above, you may prove directly that $x\in A\cap (B\cup C)\Leftrightarrow x\in(A\cap B)\cup (A\cap C)$. Thus, by extensionality of sets, you straightforwardly have $A\cap (B\cup C)=(A\cap B)\cup (A\cap C)$.
EDIT2: The distributive property of the logical connectives $\land,\lor$ may be verified by corresponding truth tables. It is important to note, that $\cap,\cup$ are defined operations in the theory of sets while the underlying logic(where you proceed with your reasoning with $\land,\lor$) is the first-order logic(of set theory). The distributive property of the logical connectives is a theorem of first-order logic which can then be used in your proof to apply it to propositions about the set-membership relation.
The reasoning is less circular as it is referential. In the end, you derive a property of your defined connectives by using a similar property of the connectives used inside their formal definition.