Theorem difininv

Description: Condition for the intersections of two sets with a given set to be equal. (Contributed by Thierry Arnoux, 28-Dec-2021)

	Ref	Expression
Assertion	difininv	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to A\cap B=C\cap B$$

Proof

Step	Hyp	Ref	Expression
1		indif1	$$⊢\left(A\setminus C\right)\cap B=\left(A\cap B\right)\setminus C$$
2	1	eqeq1i	$$⊢\left(A\setminus C\right)\cap B=\varnothing \leftrightarrow \left(A\cap B\right)\setminus C=\varnothing$$
3		ssdif0	$$⊢A\cap B\subseteq C\leftrightarrow \left(A\cap B\right)\setminus C=\varnothing$$
4	2 3	sylbb2	$$⊢\left(A\setminus C\right)\cap B=\varnothing \to A\cap B\subseteq C$$
5	4	adantr	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to A\cap B\subseteq C$$
6		inss2	$$⊢A\cap B\subseteq B$$
7	6	a1i	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to A\cap B\subseteq B$$
8	5 7	ssind	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to A\cap B\subseteq C\cap B$$
9		indif1	$$⊢\left(C\setminus A\right)\cap B=\left(C\cap B\right)\setminus A$$
10	9	eqeq1i	$$⊢\left(C\setminus A\right)\cap B=\varnothing \leftrightarrow \left(C\cap B\right)\setminus A=\varnothing$$
11		ssdif0	$$⊢C\cap B\subseteq A\leftrightarrow \left(C\cap B\right)\setminus A=\varnothing$$
12	10 11	sylbb2	$$⊢\left(C\setminus A\right)\cap B=\varnothing \to C\cap B\subseteq A$$
13	12	adantl	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to C\cap B\subseteq A$$
14		inss2	$$⊢C\cap B\subseteq B$$
15	14	a1i	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to C\cap B\subseteq B$$
16	13 15	ssind	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to C\cap B\subseteq A\cap B$$
17	8 16	eqssd	$$⊢\left(\left(A\setminus C\right)\cap B=\varnothing \wedge \left(C\setminus A\right)\cap B=\varnothing \right)\to A\cap B=C\cap B$$