Theorem uneqdifeq 4057

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.) (Proof shortened by JJ, 14-Jul-2021.)

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 3757	. . . . 5 |- ( B u. A ) = ( A u. B )
2		eqtr 2641	. . . . . . 7 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3	2	eqcomd 2628	. . . . . 6 |- ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4		difeq1 3721	. . . . . . 7 |- ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5		difun2 4048	. . . . . . 7 |- ( ( B u. A ) \ A ) = ( B \ A )
6		eqtr 2641	. . . . . . . 8 |- ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7		incom 3805	. . . . . . . . . . 11 |- ( A i^i B ) = ( B i^i A )
8	7	eqeq1i 2627	. . . . . . . . . 10 |- ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9		disj3 4021	. . . . . . . . . 10 |- ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10	8, 9	bitri 264	. . . . . . . . 9 |- ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11		eqtr 2641	. . . . . . . . . . 11 |- ( ( ( C \ A ) = ( B \ A ) /\ ( B \ A ) = B ) -> ( C \ A ) = B )
12	11	expcom 451	. . . . . . . . . 10 |- ( ( B \ A ) = B -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
13	12	eqcoms 2630	. . . . . . . . 9 |- ( B = ( B \ A ) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
14	10, 13	sylbi 207	. . . . . . . 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 694	. . . . . 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 706	. . . 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 482	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
21		simpl 473	. . . . . 6 |- ( ( A C_ C /\ ( C \ A ) = B ) -> A C_ C )
22		difssd 3738	. . . . . . . 8 |- ( ( C \ A ) = B -> ( C \ A ) C_ C )
23		sseq1 3626	. . . . . . . 8 |- ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
24	22, 23	mpbid 222	. . . . . . 7 |- ( ( C \ A ) = B -> B C_ C )
25	24	adantl 482	. . . . . 6 |- ( ( A C_ C /\ ( C \ A ) = B ) -> B C_ C )
26	21, 25	unssd 3789	. . . . 5 |- ( ( A C_ C /\ ( C \ A ) = B ) -> ( A u. B ) C_ C )
27		eqimss 3657	. . . . . . 7 |- ( ( C \ A ) = B -> ( C \ A ) C_ B )
28		ssundif 4052	. . . . . . 7 |- ( C C_ ( A u. B ) <-> ( C \ A ) C_ B )
29	27, 28	sylibr 224	. . . . . 6 |- ( ( C \ A ) = B -> C C_ ( A u. B ) )
30	29	adantl 482	. . . . 5 |- ( ( A C_ C /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
31	26, 30	eqssd 3620	. . . 4 |- ( ( A C_ C /\ ( C \ A ) = B ) -> ( A u. B ) = C )
32	31	ex 450	. . 3 |- ( A C_ C -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
33	32	adantr 481	. 2 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
34	20, 33	impbid 202	1 |- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  fzdifsuc  12400  hashbclem  13236  lecldbas  21023  conndisj  21219  ptuncnv  21610  ptunhmeo  21611  cldsubg  21914  icopnfcld  22571  iocmnfcld  22572  voliunlem1  23318  icombl  23332  ioombl  23333  uniioombllem4  23354  ismbf3d  23421  lhop  23779  subfacp1lem3  31164  subfacp1lem5  31166  pconnconn  31213  cvmscld  31255