difunieq

Description: The difference of unions is a subset of the union of the difference. (Contributed by ML, 29-Mar-2021)

		Ref	Expression
	Assertion	difunieq	$⊢ ⋃ A ∖ ⋃ B \subseteq ⋃ (A ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		eluni	$⊢ x \in ⋃ A \leftrightarrow \exists y (x \in y \land y \in A)$
2		eluni	$⊢ x \in ⋃ B \leftrightarrow \exists y (x \in y \land y \in B)$
3	2	notbii	$⊢ \neg x \in ⋃ B \leftrightarrow \neg \exists y (x \in y \land y \in B)$
4		alinexa	$⊢ \forall y (x \in y \to \neg y \in B) \leftrightarrow \neg \exists y (x \in y \land y \in B)$
5		nfa1	$⊢ Ⅎ y \forall y (x \in y \to \neg y \in B)$
6		sp	$⊢ \forall y (x \in y \to \neg y \in B) \to (x \in y \to \neg y \in B)$
7	6	adantrd	$⊢ \forall y (x \in y \to \neg y \in B) \to ((x \in y \land y \in A) \to \neg y \in B)$
8	7	ancld	$⊢ \forall y (x \in y \to \neg y \in B) \to ((x \in y \land y \in A) \to ((x \in y \land y \in A) \land \neg y \in B))$
9		anass	$⊢ ((x \in y \land y \in A) \land \neg y \in B) \leftrightarrow (x \in y \land (y \in A \land \neg y \in B))$
10	8 9	imbitrdi	$⊢ \forall y (x \in y \to \neg y \in B) \to ((x \in y \land y \in A) \to (x \in y \land (y \in A \land \neg y \in B)))$
11	5 10	eximd	$⊢ \forall y (x \in y \to \neg y \in B) \to (\exists y (x \in y \land y \in A) \to \exists y (x \in y \land (y \in A \land \neg y \in B)))$
12	4 11	sylbir	$⊢ \neg \exists y (x \in y \land y \in B) \to (\exists y (x \in y \land y \in A) \to \exists y (x \in y \land (y \in A \land \neg y \in B)))$
13	12	impcom	$⊢ (\exists y (x \in y \land y \in A) \land \neg \exists y (x \in y \land y \in B)) \to \exists y (x \in y \land (y \in A \land \neg y \in B))$
14	1 3 13	syl2anb	$⊢ (x \in ⋃ A \land \neg x \in ⋃ B) \to \exists y (x \in y \land (y \in A \land \neg y \in B))$
15		eldif	$⊢ x \in (⋃ A ∖ ⋃ B) \leftrightarrow (x \in ⋃ A \land \neg x \in ⋃ B)$
16		eluni	$⊢ x \in ⋃ (A ∖ B) \leftrightarrow \exists y (x \in y \land y \in (A ∖ B))$
17		eldif	$⊢ y \in (A ∖ B) \leftrightarrow (y \in A \land \neg y \in B)$
18	17	anbi2i	$⊢ (x \in y \land y \in (A ∖ B)) \leftrightarrow (x \in y \land (y \in A \land \neg y \in B))$
19	18	exbii	$⊢ \exists y (x \in y \land y \in (A ∖ B)) \leftrightarrow \exists y (x \in y \land (y \in A \land \neg y \in B))$
20	16 19	bitri	$⊢ x \in ⋃ (A ∖ B) \leftrightarrow \exists y (x \in y \land (y \in A \land \neg y \in B))$
21	14 15 20	3imtr4i	$⊢ x \in (⋃ A ∖ ⋃ B) \to x \in ⋃ (A ∖ B)$
22	21	ssriv	$⊢ ⋃ A ∖ ⋃ B \subseteq ⋃ (A ∖ B)$

Metamath Proof Explorer

Theorem difunieq

Proof