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

Proof

Step Hyp Ref Expression
1 eqimss ⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
2 unss ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
3 ssin ⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ↔ 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) )
4 sstr ⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
5 3 4 sylbir ⊢ ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) → 𝐴 ⊆ 𝐵 )
6 ssin ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) ↔ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) )
7 simpl ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐵 ) → 𝐵 ⊆ 𝐴 )
8 6 7 sylbir ⊢ ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) → 𝐵 ⊆ 𝐴 )
9 5 8 anim12i ⊢ ( ( 𝐴 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
10 2 9 sylbir ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
11 1 10 syl ⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
12 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
13 11 12 sylibr ⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) → 𝐴 = 𝐵 )
14 unidm ⊢ ( 𝐴 ∪ 𝐴 ) = 𝐴
15 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
16 14 15 eqtr4i ⊢ ( 𝐴 ∪ 𝐴 ) = ( 𝐴 ∩ 𝐴 )
17 uneq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) )
18 ineq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) )
19 16 17 18 3eqtr3a ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) )
20 13 19 impbii ⊢ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∩ 𝐵 ) ↔ 𝐴 = 𝐵 )