Metamath Proof Explorer

Theorem unineq

Description: Infer equality from equalities of union and intersection. Exercise 20 of Enderton p. 32 and its converse. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion unineq 
|- ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) <-> A = B )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( ( A i^i C ) = ( B i^i C ) -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) )
2 elin 
 |-  ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
3 elin 
 |-  ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
4 1 2 3 3bitr3g 
 |-  ( ( A i^i C ) = ( B i^i C ) -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) )
5 iba 
 |-  ( x e. C -> ( x e. A <-> ( x e. A /\ x e. C ) ) )
6 iba 
 |-  ( x e. C -> ( x e. B <-> ( x e. B /\ x e. C ) ) )
7 5 6 bibi12d 
 |-  ( x e. C -> ( ( x e. A <-> x e. B ) <-> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) ) )
8 4 7 imbitrrid 
 |-  ( x e. C -> ( ( A i^i C ) = ( B i^i C ) -> ( x e. A <-> x e. B ) ) )
9 8 adantld 
 |-  ( x e. C -> ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) -> ( x e. A <-> x e. B ) ) )
10 uncom 
 |-  ( A u. C ) = ( C u. A )
11 uncom 
 |-  ( B u. C ) = ( C u. B )
12 10 11 eqeq12i 
 |-  ( ( A u. C ) = ( B u. C ) <-> ( C u. A ) = ( C u. B ) )
13 eleq2 
 |-  ( ( C u. A ) = ( C u. B ) -> ( x e. ( C u. A ) <-> x e. ( C u. B ) ) )
14 12 13 sylbi 
 |-  ( ( A u. C ) = ( B u. C ) -> ( x e. ( C u. A ) <-> x e. ( C u. B ) ) )
15 elun 
 |-  ( x e. ( C u. A ) <-> ( x e. C \/ x e. A ) )
16 elun 
 |-  ( x e. ( C u. B ) <-> ( x e. C \/ x e. B ) )
17 14 15 16 3bitr3g 
 |-  ( ( A u. C ) = ( B u. C ) -> ( ( x e. C \/ x e. A ) <-> ( x e. C \/ x e. B ) ) )
18 biorf 
 |-  ( -. x e. C -> ( x e. A <-> ( x e. C \/ x e. A ) ) )
19 biorf 
 |-  ( -. x e. C -> ( x e. B <-> ( x e. C \/ x e. B ) ) )
20 18 19 bibi12d 
 |-  ( -. x e. C -> ( ( x e. A <-> x e. B ) <-> ( ( x e. C \/ x e. A ) <-> ( x e. C \/ x e. B ) ) ) )
21 17 20 imbitrrid 
 |-  ( -. x e. C -> ( ( A u. C ) = ( B u. C ) -> ( x e. A <-> x e. B ) ) )
22 21 adantrd 
 |-  ( -. x e. C -> ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) -> ( x e. A <-> x e. B ) ) )
23 9 22 pm2.61i 
 |-  ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) -> ( x e. A <-> x e. B ) )
24 23 eqrdv 
 |-  ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) -> A = B )
25 uneq1 
 |-  ( A = B -> ( A u. C ) = ( B u. C ) )
26 ineq1 
 |-  ( A = B -> ( A i^i C ) = ( B i^i C ) )
27 25 26 jca 
 |-  ( A = B -> ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) )
28 24 27 impbii 
 |-  ( ( ( A u. C ) = ( B u. C ) /\ ( A i^i C ) = ( B i^i C ) ) <-> A = B )