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