Theorem difeq

Description: Rewriting an equation with class difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017)

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

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A\setminus B=C\to \left(A\setminus B\right)\cap B=C\cap B$$
2		disjdifr	$$⊢\left(A\setminus B\right)\cap B=\varnothing$$
3	1 2	eqtr3di	$$⊢A\setminus B=C\to C\cap B=\varnothing$$
4		uneq1	$$⊢A\setminus B=C\to \left(A\setminus B\right)\cup B=C\cup B$$
5		undif1	$$⊢\left(A\setminus B\right)\cup B=A\cup B$$
6	4 5	eqtr3di	$$⊢A\setminus B=C\to C\cup B=A\cup B$$
7	3 6	jca	$$⊢A\setminus B=C\to \left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)$$
8		simpl	$$⊢\left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)\to C\cap B=\varnothing$$
9		disj3	$$⊢C\cap B=\varnothing \leftrightarrow C=C\setminus B$$
10		eqcom	$$⊢C=C\setminus B\leftrightarrow C\setminus B=C$$
11	9 10	bitri	$$⊢C\cap B=\varnothing \leftrightarrow C\setminus B=C$$
12	8 11	sylib	$$⊢\left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)\to C\setminus B=C$$
13		difeq1	$$⊢C\cup B=A\cup B\to \left(C\cup B\right)\setminus B=\left(A\cup B\right)\setminus B$$
14		difun2	$$⊢\left(C\cup B\right)\setminus B=C\setminus B$$
15		difun2	$$⊢\left(A\cup B\right)\setminus B=A\setminus B$$
16	13 14 15	3eqtr3g	$$⊢C\cup B=A\cup B\to C\setminus B=A\setminus B$$
17	16	eqeq1d	$$⊢C\cup B=A\cup B\to \left(C\setminus B=C\leftrightarrow A\setminus B=C\right)$$
18	17	adantl	$$⊢\left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)\to \left(C\setminus B=C\leftrightarrow A\setminus B=C\right)$$
19	12 18	mpbid	$$⊢\left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)\to A\setminus B=C$$
20	7 19	impbii	$$⊢A\setminus B=C\leftrightarrow \left(C\cap B=\varnothing \wedge C\cup B=A\cup B\right)$$