Theorem uneqdifeq 3884

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 3610	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2448	. . . . . . 7 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3	2	eqcomd 2430	. . . . . 6 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4		difeq1 3576	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 3875	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2448	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3655	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2429	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 3837	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 252	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2448	. . . . . . . . . . 11 |- ( ( ( C \ A ) = ( B \ A ) /\ ( B \ A ) = B ) -> ( C \ A ) = B )
12	11	expcom 436	. . . . . . . . . 10 |- ( ( B \ A ) = B -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
13	12	eqcoms 2434	. . . . . . . . 9 |- ( B = ( B \ A ) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
14	10, 13	sylbi 198	. . . . . . . 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 666	. . . . . 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 674	. . . 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 467	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
21		difss 3592	. . . . . . . 8 |- ( C \ A ) C_ C
22		sseq1 3485	. . . . . . . . 9 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
23		unss 3640	. . . . . . . . . . 11 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )
24	23	biimpi 197	. . . . . . . . . 10 |- ( ( A C_ C /\ B C_ C ) -> ( A u. B ) C_ C )
25	24	expcom 436	. . . . . . . . 9 |- ( B C_ C -> ( A C_ C -> ( A u. B ) C_ C ) )
26	22, 25	syl6bi 231	. . . . . . . 8 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C -> ( A C_ C -> ( A u. B ) C_ C ) ) )
27	21, 26	mpi 21	. . . . . . 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 466	. . . . 5 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) C_ C ) )
30	29	imp 430	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) C_ C )
31		eqimss 3516	. . . . . . 7 |- ( ( C \ A ) = B -> ( C \ A ) C_ B )
32	31	adantl 467	. . . . . 6 |- ( ( A C_ C /\ ( C \ A ) = B ) -> ( C \ A ) C_ B )
33		ssundif 3879	. . . . . 6 |- ( C C_ ( A u. B ) <-> ( C \ A ) C_ B )
34	32, 33	sylibr 215	. . . . 5 |- ( ( A C_ C /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
35	34	adantlr 719	. . . 4 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
36	30, 35	eqssd 3481	. . 3 |- ( ( ( A C_ C /\ ( A i^i B ) = (/) ) /\ ( C \ A ) = B ) -> ( A u. B ) = C )
37	36	ex 435	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
38	20, 37	impbid 193	1 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762

This theorem is referenced by:  fzdifsuc  11855  hashbclem  12612  lecldbas  20221  conndisj  20417  ptuncnv  20808  ptunhmeo  20809  cldsubg  21111  icopnfcld  21774  iocmnfcld  21775  voliunlem1  22489  icombl  22503  ioombl  22504  uniioombllem4  22530  ismbf3d  22596  lhop  22954  subfacp1lem3  29900  subfacp1lem5  29902  pconcon  29949  cvmscld  29991