Su prueba de la dirección se ve perfectamente bien. Es muy común usar "y" y "o" escritos en una prueba a nivel meta. Sin embargo, si siente que esto dificulta la presentación de un argumento, puede beneficiarse con un poco más de formalismo, por ejemplo.
\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}
Estoy usando $\land,\lor$ aquí como símbolos de "y" y "o" respectivamente.
En este caso específico, la prueba se basa en el uso de la propiedad distributiva de $\land,\lor$ como conectores lógicos para demostrar la propiedad correspondiente de uniones e intersecciones a través de la membresía en conjuntos. (esta conexión, por supuesto, no sorprende debido a la conexión común con el álgebra booleana).
Entonces, tener esta traducción de conectivos/operaciones muy similares entre sí como la esencia de una prueba puede parecer un poco ambiguo, aunque es el corazón del argumento.
En general, creo que la clave para una exposición clara siempre depende del contexto, pero casi siempre es una buena mezcla de formato, formalismo y no formalismo.
Por ejemplo, nadie quiere escribir declaraciones precisas de teoría de conjuntos de primer orden para cada concepto matemático, aunque sería formalmente estricto. En casos como el anterior, o en general con cadenas de implicaciones o bi-implicaciones, un formato estructurado de los pasos, como la presentación alineada arriba, ya puede mejorar bastante la exposición.
EDICIÓN: Nota, que puedes convertir cada implicación en la cadena anterior en una bi-implicación, es decir, por el argumento anterior, puedes probar directamente que $x\in A\cap (B\cup C)\Leftrightarrow x\in(A\cap B)\cup (A\cap C)$. Así, por la extensionalidad de conjuntos, tienes directamente $A\cap (B\cup C)=(A\cap B)\cup (A\cap C)$.
EDICIÓN2: La propiedad distributiva de los conectivos lógicos $\land,\lor$ se puede verificar mediante las correspondientes tablas de verdad. Es importante tener en cuenta que $\cap,\cup$ son operaciones definidas en la teoría de conjuntos mientras que la lógica subyacente (donde procedes con tu razonamiento con $\land,\lor$) es la lógica de primer orden (de la teoría de conjuntos). La propiedad distributiva de los conectivos lógicos es un teorema de la lógica de primer orden que luego se puede utilizar en tu prueba para aplicarlo a proposiciones sobre la relación de membresía en conjuntos.
El razonamiento es menos circular que referencial. Al final, derivas una propiedad de tus conectivos definidos utilizando una propiedad similar de los conectivos utilizados en su definición formal.
