Metamath Proof Explorer

Theorem iundif2

Description: Indexed union of class difference. Generalization of half of theorem "De Morgan's laws" in Enderton p. 31. Use intiin to recover Enderton's theorem. (Contributed by NM, 19-Aug-2004)

		Ref	Expression
	Assertion	iundif2	$⊢ ⋃_{x \in A} (B ∖ C) = B ∖ ⋂_{x \in A} C$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in C)$
2	1	rexbii	$⊢ \exists x \in A y \in (B ∖ C) \leftrightarrow \exists x \in A (y \in B \land \neg y \in C)$
3		r19.42v	$⊢ \exists x \in A (y \in B \land \neg y \in C) \leftrightarrow (y \in B \land \exists x \in A \neg y \in C)$
4		rexnal	$⊢ \exists x \in A \neg y \in C \leftrightarrow \neg \forall x \in A y \in C$
5		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C)$
6	5	elv	$⊢ y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C$
7	4 6	xchbinxr	$⊢ \exists x \in A \neg y \in C \leftrightarrow \neg y \in ⋂_{x \in A} C$
8	7	anbi2i	$⊢ (y \in B \land \exists x \in A \neg y \in C) \leftrightarrow (y \in B \land \neg y \in ⋂_{x \in A} C)$
9	2 3 8	3bitri	$⊢ \exists x \in A y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in ⋂_{x \in A} C)$
10		eliun	$⊢ y \in ⋃_{x \in A} (B ∖ C) \leftrightarrow \exists x \in A y \in (B ∖ C)$
11		eldif	$⊢ y \in (B ∖ ⋂_{x \in A} C) \leftrightarrow (y \in B \land \neg y \in ⋂_{x \in A} C)$
12	9 10 11	3bitr4i	$⊢ y \in ⋃_{x \in A} (B ∖ C) \leftrightarrow y \in (B ∖ ⋂_{x \in A} C)$
13	12	eqriv	$⊢ ⋃_{x \in A} (B ∖ C) = B ∖ ⋂_{x \in A} C$