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		ineqcom	$$⊢A\cap B=\varnothing \leftrightarrow B\cap A=\varnothing$$
8		disj3	$$⊢B\cap A=\varnothing \leftrightarrow B=B\setminus A$$
9	7 8	bitri	$$⊢A\cap B=\varnothing \leftrightarrow B=B\setminus A$$
10		eqtr	$$⊢\left(C\setminus A=B\setminus A\wedge B\setminus A=B\right)\to C\setminus A=B$$
11	10	expcom	$$⊢B\setminus A=B\to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
12	11	eqcoms	$$⊢B=B\setminus A\to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
13	9 12	sylbi	$$⊢A\cap B=\varnothing \to \left(C\setminus A=B\setminus A\to C\setminus A=B\right)$$
14	6 13	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)$$
15	4 5 14	sylancl	$$⊢C=B\cup A\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
16	3 15	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)$$
17	1 16	mpan	$$⊢A\cup B=C\to \left(A\cap B=\varnothing \to C\setminus A=B\right)$$
18	17	com12	$$⊢A\cap B=\varnothing \to \left(A\cup B=C\to C\setminus A=B\right)$$
19	18	adantl	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(A\cup B=C\to C\setminus A=B\right)$$
20		simpl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\subseteq C$$
21		difssd	$$⊢C\setminus A=B\to C\setminus A\subseteq C$$
22		sseq1	$$⊢C\setminus A=B\to \left(C\setminus A\subseteq C\leftrightarrow B\subseteq C\right)$$
23	21 22	mpbid	$$⊢C\setminus A=B\to B\subseteq C$$
24	23	adantl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to B\subseteq C$$
25	20 24	unssd	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\cup B\subseteq C$$
26		eqimss	$$⊢C\setminus A=B\to C\setminus A\subseteq B$$
27		ssundif	$$⊢C\subseteq A\cup B\leftrightarrow C\setminus A\subseteq B$$
28	26 27	sylibr	$$⊢C\setminus A=B\to C\subseteq A\cup B$$
29	28	adantl	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to C\subseteq A\cup B$$
30	25 29	eqssd	$$⊢\left(A\subseteq C\wedge C\setminus A=B\right)\to A\cup B=C$$
31	30	ex	$$⊢A\subseteq C\to \left(C\setminus A=B\to A\cup B=C\right)$$
32	31	adantr	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(C\setminus A=B\to A\cup B=C\right)$$
33	19 32	impbid	$$⊢\left(A\subseteq C\wedge A\cap B=\varnothing \right)\to \left(A\cup B=C\leftrightarrow C\setminus A=B\right)$$