Theorem uneqdifeq 4499

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 4168	. . . . 5 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
2		eqtr 2758	. . . . . . 7 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶)
3	2	eqcomd 2741	. . . . . 6 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴))
4		difeq1 4129	. . . . . . 7 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴))
5		difun2 4487	. . . . . . 7 ⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)
6		eqtr 2758	. . . . . . . 8 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴))
7		incom 4217	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
8	7	eqeq1i 2740	. . . . . . . . . 10 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
9		disj3 4460	. . . . . . . . . 10 ⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
10	8, 9	bitri 275	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
11		eqtr 2758	. . . . . . . . . . 11 ⊢ (((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) ∧ (𝐵 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) = 𝐵)
12	11	expcom 413	. . . . . . . . . 10 ⊢ ((𝐵 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
13	12	eqcoms 2743	. . . . . . . . 9 ⊢ (𝐵 = (𝐵 ∖ 𝐴) → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
14	10, 13	sylbi 217	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
15	6, 14	syl5com 31	. . . . . . 7 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
16	4, 5, 15	sylancl 586	. . . . . 6 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
17	3, 16	syl 17	. . . . 5 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
18	1, 17	mpan 690	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
19	18	com12 32	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
20	19	adantl 481	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
21		simpl 482	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐴 ⊆ 𝐶)
22		difssd 4147	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐶)
23		sseq1 4021	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
24	22, 23	mpbid 232	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐵 ⊆ 𝐶)
25	24	adantl 481	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐵 ⊆ 𝐶)
26	21, 25	unssd 4202	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
27		eqimss 4054	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵)
28		ssundif 4494	. . . . . . 7 ⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵)
29	27, 28	sylibr 234	. . . . . 6 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐶 ⊆ (𝐴 ∪ 𝐵))
30	29	adantl 481	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵))
31	26, 30	eqssd 4013	. . . 4 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) = 𝐶)
32	31	ex 412	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
33	32	adantr 480	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
34	20, 33	impbid 212	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340

This theorem is referenced by:  fzdifsuc  13621  hashbclem  14488  lecldbas  23243  conndisj  23440  ptuncnv  23831  ptunhmeo  23832  cldsubg  24135  icopnfcld  24804  iocmnfcld  24805  voliunlem1  25599  icombl  25613  ioombl  25614  uniioombllem4  25635  ismbf3d  25703  lhop  26070  symgcom  33086  f1resfz0f1d  35098  subfacp1lem3  35167  subfacp1lem5  35169  pconnconn  35216  cvmscld  35258