Theorem uneqdifeq 4396

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 4080	. . . . 5 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
2		eqtr 2818	. . . . . . 7 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶)
3	2	eqcomd 2804	. . . . . 6 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴))
4		difeq1 4043	. . . . . . 7 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴))
5		difun2 4387	. . . . . . 7 ⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)
6		eqtr 2818	. . . . . . . 8 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴))
7		incom 4128	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
8	7	eqeq1i 2803	. . . . . . . . . 10 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
9		disj3 4361	. . . . . . . . . 10 ⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
10	8, 9	bitri 278	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
11		eqtr 2818	. . . . . . . . . . 11 ⊢ (((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) ∧ (𝐵 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) = 𝐵)
12	11	expcom 417	. . . . . . . . . 10 ⊢ ((𝐵 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
13	12	eqcoms 2806	. . . . . . . . 9 ⊢ (𝐵 = (𝐵 ∖ 𝐴) → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
14	10, 13	sylbi 220	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
15	6, 14	syl5com 31	. . . . . . 7 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
16	4, 5, 15	sylancl 589	. . . . . 6 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
17	3, 16	syl 17	. . . . 5 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
18	1, 17	mpan 689	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
19	18	com12 32	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
20	19	adantl 485	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
21		simpl 486	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐴 ⊆ 𝐶)
22		difssd 4060	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐶)
23		sseq1 3940	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
24	22, 23	mpbid 235	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐵 ⊆ 𝐶)
25	24	adantl 485	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐵 ⊆ 𝐶)
26	21, 25	unssd 4113	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
27		eqimss 3971	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵)
28		ssundif 4391	. . . . . . 7 ⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵)
29	27, 28	sylibr 237	. . . . . 6 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐶 ⊆ (𝐴 ∪ 𝐵))
30	29	adantl 485	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵))
31	26, 30	eqssd 3932	. . . 4 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) = 𝐶)
32	31	ex 416	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
33	32	adantr 484	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
34	20, 33	impbid 215	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244

This theorem is referenced by:  fzdifsuc  12962  hashbclem  13806  lecldbas  21824  conndisj  22021  ptuncnv  22412  ptunhmeo  22413  cldsubg  22716  icopnfcld  23373  iocmnfcld  23374  voliunlem1  24154  icombl  24168  ioombl  24169  uniioombllem4  24190  ismbf3d  24258  lhop  24619  symgcom  30777  f1resfz0f1d  32471  subfacp1lem3  32542  subfacp1lem5  32544  pconnconn  32591  cvmscld  32633