Theorem 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	$$⊢\left(A\subseteq A\cap B\wedge B\subseteq A\cap B\right)\leftrightarrow A\cup B\subseteq A\cap B$$
3		ssin	$$⊢\left(A\subseteq A\wedge A\subseteq B\right)\leftrightarrow A\subseteq A\cap B$$
4		sstr	$$⊢\left(A\subseteq A\wedge A\subseteq B\right)\to A\subseteq B$$
5	3 4	sylbir	$$⊢A\subseteq A\cap B\to A\subseteq B$$
6		ssin	$$⊢\left(B\subseteq A\wedge B\subseteq B\right)\leftrightarrow B\subseteq A\cap B$$
7		simpl	$$⊢\left(B\subseteq A\wedge B\subseteq B\right)\to B\subseteq A$$
8	6 7	sylbir	$$⊢B\subseteq A\cap B\to B\subseteq A$$
9	5 8	anim12i	$$⊢\left(A\subseteq A\cap B\wedge B\subseteq A\cap B\right)\to \left(A\subseteq B\wedge B\subseteq A\right)$$
10	2 9	sylbir	$$⊢A\cup B\subseteq A\cap B\to \left(A\subseteq B\wedge B\subseteq A\right)$$
11	1 10	syl	$$⊢A\cup B=A\cap B\to \left(A\subseteq B\wedge B\subseteq A\right)$$
12		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
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$$