Theorem unineq 2251

Description: Infer equality from equalities of union and intersection. Exercise 20 of [Enderton] p. 32 and its converse.

Assertion

Ref	Expression
unineq	⊢ (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) ↔ A = B)

Proof of Theorem unineq

Step	Hyp	Ref	Expression
1		iba 641	. . . . . . 7 ⊢ (x ∈ C → (x ∈ A ↔ (x ∈ A ⋀ x ∈ C)))
2		iba 641	. . . . . . 7 ⊢ (x ∈ C → (x ∈ B ↔ (x ∈ B ⋀ x ∈ C)))
3	1, 2	bibi12d 628	. . . . . 6 ⊢ (x ∈ C → ((x ∈ A ↔ x ∈ B) ↔ ((x ∈ A ⋀ x ∈ C) ↔ (x ∈ B ⋀ x ∈ C))))
4		eleq2 1532	. . . . . . 7 ⊢ ((A ∩ C) = (B ∩ C) → (x ∈ (A ∩ C) ↔ x ∈ (B ∩ C)))
5		elin 2203	. . . . . . 7 ⊢ (x ∈ (A ∩ C) ↔ (x ∈ A ⋀ x ∈ C))
6		elin 2203	. . . . . . 7 ⊢ (x ∈ (B ∩ C) ↔ (x ∈ B ⋀ x ∈ C))
7	4, 5, 6	3bitr3g 553	. . . . . 6 ⊢ ((A ∩ C) = (B ∩ C) → ((x ∈ A ⋀ x ∈ C) ↔ (x ∈ B ⋀ x ∈ C)))
8	3, 7	syl5bir 210	. . . . 5 ⊢ (x ∈ C → ((A ∩ C) = (B ∩ C) → (x ∈ A ↔ x ∈ B)))
9	8	adantld 390	. . . 4 ⊢ (x ∈ C → (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) → (x ∈ A ↔ x ∈ B)))
10		biorf 734	. . . . . . 7 ⊢ (¬ x ∈ C → (x ∈ A ↔ (x ∈ C ⋁ x ∈ A)))
11		biorf 734	. . . . . . 7 ⊢ (¬ x ∈ C → (x ∈ B ↔ (x ∈ C ⋁ x ∈ B)))
12	10, 11	bibi12d 628	. . . . . 6 ⊢ (¬ x ∈ C → ((x ∈ A ↔ x ∈ B) ↔ ((x ∈ C ⋁ x ∈ A) ↔ (x ∈ C ⋁ x ∈ B))))
13		uncom 2172	. . . . . . . . 9 ⊢ (A ∪ C) = (C ∪ A)
14		uncom 2172	. . . . . . . . 9 ⊢ (B ∪ C) = (C ∪ B)
15	13, 14	eqeq12i 1485	. . . . . . . 8 ⊢ ((A ∪ C) = (B ∪ C) ↔ (C ∪ A) = (C ∪ B))
16		eleq2 1532	. . . . . . . 8 ⊢ ((C ∪ A) = (C ∪ B) → (x ∈ (C ∪ A) ↔ x ∈ (C ∪ B)))
17	15, 16	sylbi 199	. . . . . . 7 ⊢ ((A ∪ C) = (B ∪ C) → (x ∈ (C ∪ A) ↔ x ∈ (C ∪ B)))
18		elun 2169	. . . . . . 7 ⊢ (x ∈ (C ∪ A) ↔ (x ∈ C ⋁ x ∈ A))
19		elun 2169	. . . . . . 7 ⊢ (x ∈ (C ∪ B) ↔ (x ∈ C ⋁ x ∈ B))
20	17, 18, 19	3bitr3g 553	. . . . . 6 ⊢ ((A ∪ C) = (B ∪ C) → ((x ∈ C ⋁ x ∈ A) ↔ (x ∈ C ⋁ x ∈ B)))
21	12, 20	syl5bir 210	. . . . 5 ⊢ (¬ x ∈ C → ((A ∪ C) = (B ∪ C) → (x ∈ A ↔ x ∈ B)))
22	21	adantrd 391	. . . 4 ⊢ (¬ x ∈ C → (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) → (x ∈ A ↔ x ∈ B)))
23	9, 22	pm2.61i 126	. . 3 ⊢ (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) → (x ∈ A ↔ x ∈ B))
24	23	eqrdv 1471	. 2 ⊢ (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) → A = B)
25		uneq1 2173	. . 3 ⊢ (A = B → (A ∪ C) = (B ∪ C))
26		ineq1 2206	. . 3 ⊢ (A = B → (A ∩ C) = (B ∩ C))
27	25, 26	jca 288	. 2 ⊢ (A = B → ((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)))
28	24, 27	impbi 157	1 ⊢ (((A ∪ C) = (B ∪ C) ⋀ (A ∩ C) = (B ∩ C)) ↔ A = B)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223   = wceq 954   ∈ wcel 956   ∪ cun 2041   ∩ cin 2042

This theorem is referenced by:  mapdom2 4480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-in 2047

Copyright terms: Public domain