This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inssdif0

Description: Intersection, subclass, and difference relationship. (Contributed by NM, 27-Oct-1996) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by Wolf Lammen, 30-Sep-2014)

		Ref	Expression
	Assertion	inssdif0	$⊢ A \cap B \subseteq C \leftrightarrow A \cap (B ∖ C) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
2	1	imbi1i	$⊢ (x \in (A \cap B) \to x \in C) \leftrightarrow ((x \in A \land x \in B) \to x \in C)$
3		iman	$⊢ ((x \in A \land x \in B) \to x \in C) \leftrightarrow \neg ((x \in A \land x \in B) \land \neg x \in C)$
4	2 3	bitri	$⊢ (x \in (A \cap B) \to x \in C) \leftrightarrow \neg ((x \in A \land x \in B) \land \neg x \in C)$
5		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
6	5	anbi2i	$⊢ (x \in A \land x \in (B ∖ C)) \leftrightarrow (x \in A \land (x \in B \land \neg x \in C))$
7		elin	$⊢ x \in (A \cap (B ∖ C)) \leftrightarrow (x \in A \land x \in (B ∖ C))$
8		anass	$⊢ ((x \in A \land x \in B) \land \neg x \in C) \leftrightarrow (x \in A \land (x \in B \land \neg x \in C))$
9	6 7 8	3bitr4ri	$⊢ ((x \in A \land x \in B) \land \neg x \in C) \leftrightarrow x \in (A \cap (B ∖ C))$
10	4 9	xchbinx	$⊢ (x \in (A \cap B) \to x \in C) \leftrightarrow \neg x \in (A \cap (B ∖ C))$
11	10	albii	$⊢ \forall x (x \in (A \cap B) \to x \in C) \leftrightarrow \forall x \neg x \in (A \cap (B ∖ C))$
12		df-ss	$⊢ A \cap B \subseteq C \leftrightarrow \forall x (x \in (A \cap B) \to x \in C)$
13		eq0	$⊢ A \cap (B ∖ C) = \emptyset \leftrightarrow \forall x \neg x \in (A \cap (B ∖ C))$
14	11 12 13	3bitr4i	$⊢ A \cap B \subseteq C \leftrightarrow A \cap (B ∖ C) = \emptyset$