ssundif

Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007)

		Ref	Expression
	Assertion	ssundif	$⊢ A \subseteq B \cup C \leftrightarrow A ∖ B \subseteq C$

Step	Hyp	Ref	Expression
1		pm5.6	$⊢ ((x \in A \land \neg x \in B) \to x \in C) \leftrightarrow (x \in A \to (x \in B \lor x \in C))$
2		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
3	2	imbi1i	$⊢ (x \in (A ∖ B) \to x \in C) \leftrightarrow ((x \in A \land \neg x \in B) \to x \in C)$
4		elun	$⊢ x \in (B \cup C) \leftrightarrow (x \in B \lor x \in C)$
5	4	imbi2i	$⊢ (x \in A \to x \in (B \cup C)) \leftrightarrow (x \in A \to (x \in B \lor x \in C))$
6	1 3 5	3bitr4ri	$⊢ (x \in A \to x \in (B \cup C)) \leftrightarrow (x \in (A ∖ B) \to x \in C)$
7	6	albii	$⊢ \forall x (x \in A \to x \in (B \cup C)) \leftrightarrow \forall x (x \in (A ∖ B) \to x \in C)$
8		df-ss	$⊢ A \subseteq B \cup C \leftrightarrow \forall x (x \in A \to x \in (B \cup C))$
9		df-ss	$⊢ A ∖ B \subseteq C \leftrightarrow \forall x (x \in (A ∖ B) \to x \in C)$
10	7 8 9	3bitr4i	$⊢ A \subseteq B \cup C \leftrightarrow A ∖ B \subseteq C$

Metamath Proof Explorer