Theorem uneqdifeq 3868

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 3590	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2481	. . . . . . 7 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3	2	eqcomd 2468	. . . . . 6 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4		difeq1 3556	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 3859	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2481	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3637	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2467	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 3821	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 257	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2481	. . . . . . . . . . 11 |- ( ( ( C \ A ) = ( B \ A ) /\ ( B \ A ) = B ) -> ( C \ A ) = B )
12	11	expcom 441	. . . . . . . . . 10 |- ( ( B \ A ) = B -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
13	12	eqcoms 2470	. . . . . . . . 9 |- ( B = ( B \ A ) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
14	10, 13	sylbi 200	. . . . . . . 8 |- ( ( A i^i B ) = (/) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
15	6, 14	syl5com 31	. . . . . . 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 673	. . . . . 6 |- ( C = ( B u. A ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
17	3, 16	syl 17	. . . . 5 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
18	1, 17	mpan 681	. . . 4 |- ( ( A u. B ) = C -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
19	18	com12 32	. . 3 |- ( ( A i^i B ) = (/) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
20	19	adantl 472	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
21		difss 3572	. . . . . . . 8 |- ( C \ A ) C_ C
22		sseq1 3465	. . . . . . . . 9 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
23		unss 3620	. . . . . . . . . . 11 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
24	23	biimpi 199	. . . . . . . . . 10 |- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
25	24	expcom 441	. . . . . . . . 9 |- ( B C_ C -> ( A C_ C -> ( A u. B ) C_ C ) )
26	22, 25	syl6bi 236	. . . . . . . 8 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C -> ( A C_ C -> ( A u. B ) C_ C ) ) )
27	21, 26	mpi 20	. . . . . . 7 |- ( ( C \ A ) = B -> ( A C_ C -> ( A u. B ) C_ C ) )
28	27	com12 32	. . . . . 6 |- ( A C_ C -> ( ( C \ A ) = B -> ( A u. B ) C_ C ) )
29	28	adantr 471	. . . . 5 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) C_ C ) )
30	29	imp 435	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) C_ C )
31		eqimss 3496	. . . . . . 7 |- ( ( C \ A ) = B -> ( C \ A ) C_ B )
32	31	adantl 472	. . . . . 6 |- ( ( A C_ C /\ ( C \ A ) = B ) -> ( C \ A ) C_ B )
33		ssundif 3863	. . . . . 6 |- ( C C_ ( A u. B ) <-> ( C \ A ) C_ B )
34	32, 33	sylibr 217	. . . . 5 |- ( ( A C_ C /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
35	34	adantlr 726	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
36	30, 35	eqssd 3461	. . 3 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) = C )
37	36	ex 440	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
38	20, 37	impbid 195	1 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   \ cdif 3413   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744

This theorem is referenced by:  fzdifsuc  11884  hashbclem  12648  lecldbas  20284  conndisj  20480  ptuncnv  20871  ptunhmeo  20872  cldsubg  21174  icopnfcld  21837  iocmnfcld  21838  voliunlem1  22552  icombl  22566  ioombl  22567  uniioombllem4  22593  ismbf3d  22659  lhop  23017  subfacp1lem3  29954  subfacp1lem5  29956  pconcon  30003  cvmscld  30045