Theorem indifbi

Description: Two ways to express equality relative to a class A . (Contributed by Thierry Arnoux, 23-Jun-2024)

	Ref	Expression
Assertion	indifbi	$$⊢A\cap B=A\cap C\leftrightarrow A\setminus B=A\setminus C$$

Proof

Step	Hyp	Ref	Expression
1		inss1	$$⊢A\cap B\subseteq A$$
2		inss1	$$⊢A\cap C\subseteq A$$
3		rcompleq	$$⊢\left(A\cap B\subseteq A\wedge A\cap C\subseteq A\right)\to \left(A\cap B=A\cap C\leftrightarrow A\setminus \left(A\cap B\right)=A\setminus \left(A\cap C\right)\right)$$
4	1 2 3	mp2an	$$⊢A\cap B=A\cap C\leftrightarrow A\setminus \left(A\cap B\right)=A\setminus \left(A\cap C\right)$$
5		difin	$$⊢A\setminus \left(A\cap B\right)=A\setminus B$$
6		difin	$$⊢A\setminus \left(A\cap C\right)=A\setminus C$$
7	5 6	eqeq12i	$$⊢A\setminus \left(A\cap B\right)=A\setminus \left(A\cap C\right)\leftrightarrow A\setminus B=A\setminus C$$
8	4 7	bitri	$$⊢A\cap B=A\cap C\leftrightarrow A\setminus B=A\setminus C$$