Theorem uneqdifeq

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)

	Ref	Expression
Assertion	uneqdifeq	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(A\cup B=C\leftrightarrow C\setminus A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		uncom	$$⊢B\cup A=A\cup B$$
2		eqtr	$$⊢\left(B\cup A=A\cup B\wedge A\cup B=C\right)\to B\cup A=C$$
3	2	eqcomd	$$⊢\left(B\cup A=A\cup B\wedge A\cup B=C\right)\to C=B\cup A$$
4		difeq1	$$⊢C=B\cup A\to C\setminus A=\left(B\cup A\right)\setminus A$$
5		difun2	$$⊢\left(B\cup A\right)\setminus A=B\setminus A$$
6		eqtr	$$⊢\left(C\setminus A=\left(B\cup A\right)\setminus A\wedge \left(B\cup A\right)\setminus A=B\setminus A\right)\to C\setminus A=B\setminus A$$
7		incom	$$⊢A\cap B=B\cap A$$
8	7	eqeq1i	$$⊢A\cap B=\varnothing \leftrightarrow B\cap A=\varnothing$$
9		disj3	$$⊢B\cap A=\varnothing \leftrightarrow B=B\setminus A$$
10	8 9	bitri	$$⊢A\cap B=\varnothing \leftrightarrow B=B\setminus A$$
11		eqtr	$$⊢\left(C\setminus A=B\setminus A\wedge B\setminus A=B\right)\to C\setminus A=B$$
12	11	expcom	$$⊢B\setminus A=B\to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
13	12	eqcoms	$$⊢B=B\setminus A\to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
14	10 13	sylbi	$$⊢A\cap B=\varnothing \to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
15	6 14	syl5com	$$⊢\left(C\setminus A=\left(B\cup A\right)\setminus A\wedge \left(B\cup A\right)\setminus A=B\setminus A\right)\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
16	4 5 15	sylancl	$$⊢C=B\cup A\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
17	3 16	syl	$$⊢\left(B\cup A=A\cup B\wedge A\cup B=C\right)\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
18	1 17	mpan	$$⊢A\cup B=C\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
19	18	com12	$$⊢A\cap B=\varnothing \to \left(A\cup B=C\to C\setminus A=B\right)$$
20	19	adantl	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(A\cup B=C\to C\setminus A=B\right)$$
21		simpl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\subseteq C$$
22		difssd	$$⊢C\setminus A=B\to C\setminus A\subseteq C$$
23		sseq1	$$⊢C\setminus A=B\to \left(C\setminus A\subseteq C\leftrightarrow B\subseteq C\right)$$
24	22 23	mpbid	$$⊢C\setminus A=B\to B\subseteq C$$
25	24	adantl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to B\subseteq C$$
26	21 25	unssd	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\cup B\subseteq C$$
27		eqimss	$$⊢C\setminus A=B\to C\setminus A\subseteq B$$
28		ssundif	$$⊢C\subseteq A\cup B\leftrightarrow C\setminus A\subseteq B$$
29	27 28	sylibr	$$⊢C\setminus A=B\to C\subseteq A\cup B$$
30	29	adantl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to C\subseteq A\cup B$$
31	26 30	eqssd	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\cup B=C$$
32	31	ex	$$⊢A\subseteq C\to \left(C\setminus A=B\to A\cup B=C\right)$$
33	32	adantr	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(C\setminus A=B\to A\cup B=C\right)$$
34	20 33	impbid	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(A\cup B=C\leftrightarrow C\setminus A=B\right)$$