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

Metamath Proof Explorer

Theorem difin0ss

Description: Difference, intersection, and subclass relationship. (Contributed by NM, 30-Apr-1994) (Proof shortened by Wolf Lammen, 30-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		eq0	$⊢ (A ∖ B) \cap C = \emptyset \leftrightarrow \forall x \neg x \in ((A ∖ B) \cap C)$
2		iman	$⊢ (x \in C \to (x \in A \to x \in B)) \leftrightarrow \neg (x \in C \land \neg (x \in A \to x \in B))$
3		elin	$⊢ x \in ((A ∖ B) \cap C) \leftrightarrow (x \in (A ∖ B) \land x \in C)$
4		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
5	4	anbi2ci	$⊢ (x \in (A ∖ B) \land x \in C) \leftrightarrow (x \in C \land (x \in A \land \neg x \in B))$
6		annim	$⊢ (x \in A \land \neg x \in B) \leftrightarrow \neg (x \in A \to x \in B)$
7	6	anbi2i	$⊢ (x \in C \land (x \in A \land \neg x \in B)) \leftrightarrow (x \in C \land \neg (x \in A \to x \in B))$
8	3 5 7	3bitri	$⊢ x \in ((A ∖ B) \cap C) \leftrightarrow (x \in C \land \neg (x \in A \to x \in B))$
9	2 8	xchbinxr	$⊢ (x \in C \to (x \in A \to x \in B)) \leftrightarrow \neg x \in ((A ∖ B) \cap C)$
10		ax-2	$⊢ (x \in C \to (x \in A \to x \in B)) \to ((x \in C \to x \in A) \to (x \in C \to x \in B))$
11	9 10	sylbir	$⊢ \neg x \in ((A ∖ B) \cap C) \to ((x \in C \to x \in A) \to (x \in C \to x \in B))$
12	11	al2imi	$⊢ \forall x \neg x \in ((A ∖ B) \cap C) \to (\forall x (x \in C \to x \in A) \to \forall x (x \in C \to x \in B))$
13		df-ss	$⊢ C \subseteq A \leftrightarrow \forall x (x \in C \to x \in A)$
14		df-ss	$⊢ C \subseteq B \leftrightarrow \forall x (x \in C \to x \in B)$
15	12 13 14	3imtr4g	$⊢ \forall x \neg x \in ((A ∖ B) \cap C) \to (C \subseteq A \to C \subseteq B)$
16	1 15	sylbi	$⊢ (A ∖ B) \cap C = \emptyset \to (C \subseteq A \to C \subseteq B)$