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	$⊢ ((A ∖ C) \cap B = \emptyset \land (C ∖ A) \cap B = \emptyset) \to A \cap B = C \cap B$

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

Metamath Proof Explorer