uneqin

Description: Equality of union and intersection implies equality of their arguments. (Contributed by NM, 16-Apr-2006) (Proof shortened by Andrew Salmon, 26-Jun-2011)

		Ref	Expression
	Assertion	uneqin	$⊢ A \cup B = A \cap B \leftrightarrow A = B$

Proof

Step	Hyp	Ref	Expression
1		eqimss	$⊢ A \cup B = A \cap B \to A \cup B \subseteq A \cap B$
2		unss	$⊢ (A \subseteq A \cap B \land B \subseteq A \cap B) \leftrightarrow A \cup B \subseteq A \cap B$
3		ssin	$⊢ (A \subseteq A \land A \subseteq B) \leftrightarrow A \subseteq A \cap B$
4		sstr	$⊢ (A \subseteq A \land A \subseteq B) \to A \subseteq B$
5	3 4	sylbir	$⊢ A \subseteq A \cap B \to A \subseteq B$
6		ssin	$⊢ (B \subseteq A \land B \subseteq B) \leftrightarrow B \subseteq A \cap B$
7		simpl	$⊢ (B \subseteq A \land B \subseteq B) \to B \subseteq A$
8	6 7	sylbir	$⊢ B \subseteq A \cap B \to B \subseteq A$
9	5 8	anim12i	$⊢ (A \subseteq A \cap B \land B \subseteq A \cap B) \to (A \subseteq B \land B \subseteq A)$
10	2 9	sylbir	$⊢ A \cup B \subseteq A \cap B \to (A \subseteq B \land B \subseteq A)$
11	1 10	syl	$⊢ A \cup B = A \cap B \to (A \subseteq B \land B \subseteq A)$
12		eqss	$⊢ A = B \leftrightarrow (A \subseteq B \land B \subseteq A)$
13	11 12	sylibr	$⊢ A \cup B = A \cap B \to A = B$
14		unidm	$⊢ A \cup A = A$
15		inidm	$⊢ A \cap A = A$
16	14 15	eqtr4i	$⊢ A \cup A = A \cap A$
17		uneq2	$⊢ A = B \to A \cup A = A \cup B$
18		ineq2	$⊢ A = B \to A \cap A = A \cap B$
19	16 17 18	3eqtr3a	$⊢ A = B \to A \cup B = A \cap B$
20	13 19	impbii	$⊢ A \cup B = A \cap B \leftrightarrow A = B$

Metamath Proof Explorer

Theorem uneqin

Proof