Theorem rp-fakeuninass

Description: A special case where a mixture of union and intersection appears to conform to a mixed associative law. (Contributed by RP, 29-Feb-2020)

	Ref	Expression
Assertion	rp-fakeuninass	$$⊢A\subseteq C\leftrightarrow \left(A\cup B\right)\cap C=A\cup \left(B\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		rp-fakeinunass	$$⊢A\subseteq C\leftrightarrow \left(C\cap B\right)\cup A=C\cap \left(B\cup A\right)$$
2		eqcom	$$⊢\left(C\cap B\right)\cup A=C\cap \left(B\cup A\right)\leftrightarrow C\cap \left(B\cup A\right)=\left(C\cap B\right)\cup A$$
3		incom	$$⊢C\cap \left(B\cup A\right)=\left(B\cup A\right)\cap C$$
4		uncom	$$⊢B\cup A=A\cup B$$
5	4	ineq1i	$$⊢\left(B\cup A\right)\cap C=\left(A\cup B\right)\cap C$$
6	3 5	eqtri	$$⊢C\cap \left(B\cup A\right)=\left(A\cup B\right)\cap C$$
7		uncom	$$⊢\left(C\cap B\right)\cup A=A\cup \left(C\cap B\right)$$
8		incom	$$⊢C\cap B=B\cap C$$
9	8	uneq2i	$$⊢A\cup \left(C\cap B\right)=A\cup \left(B\cap C\right)$$
10	7 9	eqtri	$$⊢\left(C\cap B\right)\cup A=A\cup \left(B\cap C\right)$$
11	6 10	eqeq12i	$$⊢C\cap \left(B\cup A\right)=\left(C\cap B\right)\cup A\leftrightarrow \left(A\cup B\right)\cap C=A\cup \left(B\cap C\right)$$
12	1 2 11	3bitri	$$⊢A\subseteq C\leftrightarrow \left(A\cup B\right)\cap C=A\cup \left(B\cap C\right)$$