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 syl5ibr ( 𝑥𝐶 → ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) → ( 𝑥𝐴𝑥𝐵 ) ) )
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 syl5ibr ( ¬ 𝑥𝐶 → ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) → ( 𝑥𝐴𝑥𝐵 ) ) )
22 21 adantrd ( ¬ 𝑥𝐶 → ( ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) → ( 𝑥𝐴𝑥𝐵 ) ) )
23 9 22 pm2.61i ( ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) → ( 𝑥𝐴𝑥𝐵 ) )
24 23 eqrdv ( ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) → 𝐴 = 𝐵 )
25 uneq1 ( 𝐴 = 𝐵 → ( 𝐴𝐶 ) = ( 𝐵𝐶 ) )
26 ineq1 ( 𝐴 = 𝐵 → ( 𝐴𝐶 ) = ( 𝐵𝐶 ) )
27 25 26 jca ( 𝐴 = 𝐵 → ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) )
28 24 27 impbii ( ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ∧ ( 𝐴𝐶 ) = ( 𝐵𝐶 ) ) ↔ 𝐴 = 𝐵 )