Theorem uneqdifeq 3908

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 3641	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2486	. . . . . . 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 3608	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 3899	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2486	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3684	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2467	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 3864	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 249	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2486	. . . . . . . . . . 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 2472	. . . . . . . . 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 3624	. . . . . . . 8 |- ( C \ A ) C_ C
22		sseq1 3518	. . . . . . . . 9 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
23		unss 3671	. . . . . . . . . . 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 3549	. . . . . . 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 3903	. . . . . 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 3514	. . 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 1374   \ cdif 3466   u. cun 3467   i^i cin 3468   C_ wss 3469   (/)c0 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779

This theorem is referenced by:  fzdifsuc  11728  hashbclem  12454  lecldbas  19479  conndisj  19676  ptuncnv  20036  ptunhmeo  20037  cldsubg  20337  icopnfcld  21003  iocmnfcld  21004  voliunlem1  21688  icombl  21702  ioombl  21703  uniioombllem4  21723  ismbf3d  21789  lhop  22145  subfacp1lem3  28252  subfacp1lem5  28254  pconcon  28302  cvmscld  28344