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 u. B ) = ( A i^i B ) <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		eqimss	|- ( ( A u. B ) = ( A i^i B ) -> ( A u. B ) C_ ( A i^i B ) )
2		unss	|- ( ( A C_ ( A i^i B ) /\ B C_ ( A i^i B ) ) <-> ( A u. B ) C_ ( A i^i B ) )
3		ssin	|- ( ( A C_ A /\ A C_ B ) <-> A C_ ( A i^i B ) )
4		sstr	|- ( ( A C_ A /\ A C_ B ) -> A C_ B )
5	3 4	sylbir	|- ( A C_ ( A i^i B ) -> A C_ B )
6		ssin	|- ( ( B C_ A /\ B C_ B ) <-> B C_ ( A i^i B ) )
7		simpl	|- ( ( B C_ A /\ B C_ B ) -> B C_ A )
8	6 7	sylbir	|- ( B C_ ( A i^i B ) -> B C_ A )
9	5 8	anim12i	|- ( ( A C_ ( A i^i B ) /\ B C_ ( A i^i B ) ) -> ( A C_ B /\ B C_ A ) )
10	2 9	sylbir	|- ( ( A u. B ) C_ ( A i^i B ) -> ( A C_ B /\ B C_ A ) )
11	1 10	syl	|- ( ( A u. B ) = ( A i^i B ) -> ( A C_ B /\ B C_ A ) )
12		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
13	11 12	sylibr	|- ( ( A u. B ) = ( A i^i B ) -> A = B )
14		unidm	|- ( A u. A ) = A
15		inidm	|- ( A i^i A ) = A
16	14 15	eqtr4i	|- ( A u. A ) = ( A i^i A )
17		uneq2	|- ( A = B -> ( A u. A ) = ( A u. B ) )
18		ineq2	|- ( A = B -> ( A i^i A ) = ( A i^i B ) )
19	16 17 18	3eqtr3a	|- ( A = B -> ( A u. B ) = ( A i^i B ) )
20	13 19	impbii	|- ( ( A u. B ) = ( A i^i B ) <-> A = B )