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

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 ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) ↔ 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ) )
2 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) )
3 elin ⊢ ( 𝑥 ∈ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )
4 1 2 3 3bitr3g ⊢ ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
5 iba ⊢ ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ) )
6 iba ⊢ ( 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
7 5 6 bibi12d ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) ) )
8 4 7 imbitrrid ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
9 8 adantld ⊢ ( 𝑥 ∈ 𝐶 → ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
10 uncom ⊢ ( 𝐴 ∪ 𝐶 ) = ( 𝐶 ∪ 𝐴 )
11 uncom ⊢ ( 𝐵 ∪ 𝐶 ) = ( 𝐶 ∪ 𝐵 )
12 10 11 eqeq12i ⊢ ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐶 ∪ 𝐴 ) = ( 𝐶 ∪ 𝐵 ) )
13 eleq2 ⊢ ( ( 𝐶 ∪ 𝐴 ) = ( 𝐶 ∪ 𝐵 ) → ( 𝑥 ∈ ( 𝐶 ∪ 𝐴 ) ↔ 𝑥 ∈ ( 𝐶 ∪ 𝐵 ) ) )
14 12 13 sylbi ⊢ ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) → ( 𝑥 ∈ ( 𝐶 ∪ 𝐴 ) ↔ 𝑥 ∈ ( 𝐶 ∪ 𝐵 ) ) )
15 elun ⊢ ( 𝑥 ∈ ( 𝐶 ∪ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) )
16 elun ⊢ ( 𝑥 ∈ ( 𝐶 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐵 ) )
17 14 15 16 3bitr3g ⊢ ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) → ( ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐵 ) ) )
18 biorf ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ) )
19 biorf ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐵 ) ) )
20 18 19 bibi12d ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐶 ∨ 𝑥 ∈ 𝐵 ) ) ) )
21 17 20 imbitrrid ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
22 21 adantrd ⊢ ( ¬ 𝑥 ∈ 𝐶 → ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) )
23 9 22 pm2.61i ⊢ ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
24 23 eqrdv ⊢ ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) → 𝐴 = 𝐵 )
25 uneq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) )
26 ineq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) )
27 25 26 jca ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) )
28 24 27 impbii ⊢ ( ( ( 𝐴 ∪ 𝐶 ) = ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) ↔ 𝐴 = 𝐵 )