Prove distributive law of sets Let $A,B,C$ be sets. Prove the distributive law
$$A \cap\left(B\cup C\right) = \left(A\cap B\right)\cup \left(A\cap C\right)$$

proof
First we'll show that $A \cap\left(B\cup C\right) \subset \left(A\cap B\right)\cup \left(A\cap C\right)$, and then the converse. 
If $x$ is in $A \cap\left(B\cup C\right)$, then $x$ must be in $A$ and $x$ must be in $B$ or $C$. An element $x$ can satisfy this membership by being in either $A$ and $B$, or $A$ and $C$. In symbols, 
$$x \in \left[\left(A\cap B\right)\cup \left(A\cap C\right)\right]$$

I'm not going to write the other direction. Because I know once I have this way down I can go the other way. What I'm looking for is -- in addition to correctness -- whether my argument is clunky or ambiguous. This "or" and "and" wording throws me for a loop when I'm trying to use it as a math operation and a word. Ideally, I'd like to know if there's a simpler way to write these types of proofs. 
 A: I also struggled with the usefulness of spelling out the operations in plain English in this very proof, I feel they don't really add to the proof any more than the symbolic equations. I think you may be able to directly write:
$$
\forall x (x \in (A \cap (B \cup C)) \implies x \in ((A \cap B) \cup (B \cap C))) \implies (A \cap (B \cup C)) \subseteq  ((A \cap B) \cup (B \cap C)))
$$
$$
\forall x (x \in ((A \cap B) \cup (B \cap C)) \implies  x \in (A \cap (B \cup C)) ) \implies ((A \cap B) \cup (B \cap C))  \subseteq  (A \cap (B \cup C)) )
$$
Therefore
$$
(A \cap (B \cup C)) = ((A \cap B) \cup (B \cap C))
$$
The proof relies on only two things: (1) definition of a subset $
A \subseteq B \iff \forall x (x \in A \implies x \in B)
$ and (2) $(X \subseteq Y) \land (Y \subseteq X) \implies X = Y$
A: 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.
A: When proving "$P$ or $Q$" you can instead prove "If not $P$, then $Q$."
I cannot think of a way at the moment to simplify "$P$ and $Q$".
