Theorem uneqdifeq 3919

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 3644	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2483	. . . . . . 7 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3	2	eqcomd 2465	. . . . . 6 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4		difeq1 3611	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 3910	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2483	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3687	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2464	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 3874	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 249	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2483	. . . . . . . . . . 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 2469	. . . . . . . . 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 3627	. . . . . . . 8 |- ( C \ A ) C_ C
22		sseq1 3520	. . . . . . . . 9 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
23		unss 3674	. . . . . . . . . . 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 3551	. . . . . . 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 3914	. . . . . 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 3516	. . 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 1395   \ cdif 3468   u. cun 3469   i^i cin 3470   C_ wss 3471   (/)c0 3793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794

This theorem is referenced by:  fzdifsuc  11765  hashbclem  12505  lecldbas  19847  conndisj  20043  ptuncnv  20434  ptunhmeo  20435  cldsubg  20735  icopnfcld  21401  iocmnfcld  21402  voliunlem1  22086  icombl  22100  ioombl  22101  uniioombllem4  22121  ismbf3d  22187  lhop  22543  subfacp1lem3  28823  subfacp1lem5  28825  pconcon  28873  cvmscld  28915