Theorem uneqdifeq 4452

Description: Two ways to say that 𝐴 and 𝐵 partition 𝐶 (when 𝐴 and 𝐵 don't overlap and 𝐴 is a part of 𝐶). (Contributed by FL, 17-Nov-2008.) (Proof shortened by JJ, 14-Jul-2021.)

Assertion

Ref	Expression
uneqdifeq	⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))

Proof of Theorem uneqdifeq

Step	Hyp	Ref	Expression
1		uncom 4111	. . . . 5 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
2		eqtr 2782	. . . . . . 7 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶)
3	2	eqcomd 2768	. . . . . 6 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴))
4		difeq1 4073	. . . . . . 7 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴))
5		difun2 4441	. . . . . . 7 ⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)
6		eqtr 2782	. . . . . . . 8 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴))
7		ineqcom 4162	. . . . . . . . . 10 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
8		disj3 4413	. . . . . . . . . 10 ⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
9	7, 8	bitri 278	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
10		eqtr 2782	. . . . . . . . . . 11 ⊢ (((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) ∧ (𝐵 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) = 𝐵)
11	10	expcom 418	. . . . . . . . . 10 ⊢ ((𝐵 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
12	11	eqcoms 2770	. . . . . . . . 9 ⊢ (𝐵 = (𝐵 ∖ 𝐴) → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
13	9, 12	sylbi 220	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
14	6, 13	syl5com 32	. . . . . . 7 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
15	4, 5, 14	sylancl 597	. . . . . 6 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
16	3, 15	syl 18	. . . . 5 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
17	1, 16	mpan 702	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
18	17	com12 33	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
19	18	adantl 486	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
20		simpl 487	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐴 ⊆ 𝐶)
21		difssd 4090	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐶)
22		sseq1 3961	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
23	21, 22	mpbid 235	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐵 ⊆ 𝐶)
24	23	adantl 486	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐵 ⊆ 𝐶)
25	20, 24	unssd 4144	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
26		eqimss 3994	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵)
27		ssundif 4447	. . . . . . 7 ⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵)
28	26, 27	sylibr 237	. . . . . 6 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐶 ⊆ (𝐴 ∪ 𝐵))
29	28	adantl 486	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵))
30	25, 29	eqssd 3953	. . . 4 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) = 𝐶)
31	30	ex 417	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
32	31	adantr 485	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
33	19, 32	impbid 215	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1569   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286

This theorem is used by:  fzdifsuc  13619  hashbclem  14496  lecldbas  23387  conndisj  23584  ptuncnv  23975  ptunhmeo  23976  cldsubg  24279  icopnfcld  24935  iocmnfcld  24936  voliunlem1  25720  icombl  25734  ioombl  25735  uniioombllem4  25756  ismbf3d  25824  lhop  26186  symgcom  33412  f1resfz0f1d  35613  subfacp1lem3  35682  subfacp1lem5  35684  pconnconn  35731  cvmscld  35773