This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )