Metamath Proof Explorer

Theorem rp-fakeinunass

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

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

Proof

Step	Hyp	Ref	Expression
1		rp-fakeanorass	$⊢ (x \in C \to x \in A) \leftrightarrow (((x \in A \land x \in B) \lor x \in C) \leftrightarrow (x \in A \land (x \in B \lor x \in C)))$
2	1	albii	$⊢ \forall x (x \in C \to x \in A) \leftrightarrow \forall x (((x \in A \land x \in B) \lor x \in C) \leftrightarrow (x \in A \land (x \in B \lor x \in C)))$
3		dfss2	$⊢ C \subseteq A \leftrightarrow \forall x (x \in C \to x \in A)$
4		dfcleq	$⊢ (A \cap B) \cup C = A \cap (B \cup C) \leftrightarrow \forall x (x \in ((A \cap B) \cup C) \leftrightarrow x \in (A \cap (B \cup C)))$
5		elun	$⊢ x \in ((A \cap B) \cup C) \leftrightarrow (x \in (A \cap B) \lor x \in C)$
6		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
7	6	orbi1i	$⊢ (x \in (A \cap B) \lor x \in C) \leftrightarrow ((x \in A \land x \in B) \lor x \in C)$
8	5 7	bitri	$⊢ x \in ((A \cap B) \cup C) \leftrightarrow ((x \in A \land x \in B) \lor x \in C)$
9		elin	$⊢ x \in (A \cap (B \cup C)) \leftrightarrow (x \in A \land x \in (B \cup C))$
10		elun	$⊢ x \in (B \cup C) \leftrightarrow (x \in B \lor x \in C)$
11	10	anbi2i	$⊢ (x \in A \land x \in (B \cup C)) \leftrightarrow (x \in A \land (x \in B \lor x \in C))$
12	9 11	bitri	$⊢ x \in (A \cap (B \cup C)) \leftrightarrow (x \in A \land (x \in B \lor x \in C))$
13	8 12	bibi12i	$⊢ (x \in ((A \cap B) \cup C) \leftrightarrow x \in (A \cap (B \cup C))) \leftrightarrow (((x \in A \land x \in B) \lor x \in C) \leftrightarrow (x \in A \land (x \in B \lor x \in C)))$
14	13	albii	$⊢ \forall x (x \in ((A \cap B) \cup C) \leftrightarrow x \in (A \cap (B \cup C))) \leftrightarrow \forall x (((x \in A \land x \in B) \lor x \in C) \leftrightarrow (x \in A \land (x \in B \lor x \in C)))$
15	4 14	bitri	$⊢ (A \cap B) \cup C = A \cap (B \cup C) \leftrightarrow \forall x (((x \in A \land x \in B) \lor x \in C) \leftrightarrow (x \in A \land (x \in B \lor x \in C)))$
16	2 3 15	3bitr4i	$⊢ C \subseteq A \leftrightarrow (A \cap B) \cup C = A \cap (B \cup C)$