Theorem uneqdifeq 4444

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 4109	. . . . 5 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
2		eqtr 2755	. . . . . . 7 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶)
3	2	eqcomd 2741	. . . . . 6 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴))
4		difeq1 4070	. . . . . . 7 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴))
5		difun2 4432	. . . . . . 7 ⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)
6		eqtr 2755	. . . . . . . 8 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴))
7		incom 4160	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
8	7	eqeq1i 2740	. . . . . . . . . 10 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
9		disj3 4405	. . . . . . . . . 10 ⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
10	8, 9	bitri 275	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
11		eqtr 2755	. . . . . . . . . . 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 587	. . . . . 6 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
17	3, 16	syl 17	. . . . 5 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
18	1, 17	mpan 691	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
19	18	com12 32	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
20	19	adantl 481	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
21		simpl 482	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐴 ⊆ 𝐶)
22		difssd 4088	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐶)
23		sseq1 3958	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
24	22, 23	mpbid 232	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐵 ⊆ 𝐶)
25	24	adantl 481	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐵 ⊆ 𝐶)
26	21, 25	unssd 4143	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
27		eqimss 3991	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵)
28		ssundif 4439	. . . . . . 7 ⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵)
29	27, 28	sylibr 234	. . . . . 6 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐶 ⊆ (𝐴 ∪ 𝐵))
30	29	adantl 481	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵))
31	26, 30	eqssd 3950	. . . 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 1542   ∖ cdif 3897   ∪ cun 3898   ∩ cin 3899   ⊆ wss 3900  ∅c0 4284

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ral 3051  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285

This theorem is referenced by:  fzdifsuc  13502  hashbclem  14377  lecldbas  23165  conndisj  23362  ptuncnv  23753  ptunhmeo  23754  cldsubg  24057  icopnfcld  24713  iocmnfcld  24714  voliunlem1  25509  icombl  25523  ioombl  25524  uniioombllem4  25545  ismbf3d  25613  lhop  25979  symgcom  33144  f1resfz0f1d  35287  subfacp1lem3  35355  subfacp1lem5  35357  pconnconn  35404  cvmscld  35446