Theorem uneqdifeq 3788

Description: Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C). (Contributed by FL, 17-Nov-2008.)

Assertion

Ref	Expression
uneqdifeq	|- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Proof of Theorem uneqdifeq

Step	Hyp	Ref	Expression
1		uncom 3521	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2460	. . . . . . 7 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3	2	eqcomd 2448	. . . . . 6 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4		difeq1 3488	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 3779	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2460	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3564	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2450	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 3744	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 249	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2460	. . . . . . . . . . 11 |- ( ( ( C \ A ) = ( B \ A ) /\ ( B \ A ) = B ) -> ( C \ A ) = B )
12	11	expcom 435	. . . . . . . . . 10 |- ( ( B \ A ) = B -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
13	12	eqcoms 2446	. . . . . . . . 9 |- ( B = ( B \ A ) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
14	10, 13	sylbi 195	. . . . . . . 8 |- ( ( A i^i B ) = (/) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
15	6, 14	syl5com 30	. . . . . . 7 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
16	4, 5, 15	sylancl 662	. . . . . 6 |- ( C = ( B u. A ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
17	3, 16	syl 16	. . . . 5 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
18	1, 17	mpan 670	. . . 4 |- ( ( A u. B ) = C -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
19	18	com12 31	. . 3 |- ( ( A i^i B ) = (/) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
20	19	adantl 466	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
21		difss 3504	. . . . . . . 8 |- ( C \ A ) C_ C
22		sseq1 3398	. . . . . . . . 9 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
23		unss 3551	. . . . . . . . . . 11 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
24	23	biimpi 194	. . . . . . . . . 10 |- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
25	24	expcom 435	. . . . . . . . 9 |- ( B C_ C -> ( A C_ C -> ( A u. B ) C_ C ) )
26	22, 25	syl6bi 228	. . . . . . . 8 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C -> ( A C_ C -> ( A u. B ) C_ C ) ) )
27	21, 26	mpi 17	. . . . . . 7 |- ( ( C \ A ) = B -> ( A C_ C -> ( A u. B ) C_ C ) )
28	27	com12 31	. . . . . 6 |- ( A C_ C -> ( ( C \ A ) = B -> ( A u. B ) C_ C ) )
29	28	adantr 465	. . . . 5 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) C_ C ) )
30	29	imp 429	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) C_ C )
31		eqimss 3429	. . . . . . 7 |- ( ( C \ A ) = B -> ( C \ A ) C_ B )
32	31	adantl 466	. . . . . 6 |- ( ( A C_ C /\ ( C \ A ) = B ) -> ( C \ A ) C_ B )
33		ssundif 3783	. . . . . 6 |- ( C C_ ( A u. B ) <-> ( C \ A ) C_ B )
34	32, 33	sylibr 212	. . . . 5 |- ( ( A C_ C /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
35	34	adantlr 714	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
36	30, 35	eqssd 3394	. . 3 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) = C )
37	36	ex 434	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
38	20, 37	impbid 191	1 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   \ cdif 3346   u. cun 3347   i^i cin 3348   C_ wss 3349   (/)c0 3658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659

This theorem is referenced by:  fzdifsuc  11537  hashbclem  12226  lecldbas  18845  conndisj  19042  ptuncnv  19402  ptunhmeo  19403  cldsubg  19703  icopnfcld  20369  iocmnfcld  20370  voliunlem1  21053  icombl  21067  ioombl  21068  uniioombllem4  21088  ismbf3d  21154  lhop  21510  subfacp1lem3  27092  subfacp1lem5  27094  pconcon  27142  cvmscld  27184