Metamath Proof Explorer

Theorem iindif2

Description: Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws" in Enderton p. 31. Use uniiun to recover Enderton's theorem. (Contributed by NM, 5-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	$⊢ A \neq \emptyset \to (\forall x \in A (y \in B \land \neg y \in C) \leftrightarrow (y \in B \land \forall x \in A \neg y \in C))$
2		eldif	$⊢ y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in C)$
3	2	bicomi	$⊢ (y \in B \land \neg y \in C) \leftrightarrow y \in (B ∖ C)$
4	3	ralbii	$⊢ \forall x \in A (y \in B \land \neg y \in C) \leftrightarrow \forall x \in A y \in (B ∖ C)$
5		ralnex	$⊢ \forall x \in A \neg y \in C \leftrightarrow \neg \exists x \in A y \in C$
6		eliun	$⊢ y \in ⋃_{x \in A} C \leftrightarrow \exists x \in A y \in C$
7	5 6	xchbinxr	$⊢ \forall x \in A \neg y \in C \leftrightarrow \neg y \in ⋃_{x \in A} C$
8	7	anbi2i	$⊢ (y \in B \land \forall x \in A \neg y \in C) \leftrightarrow (y \in B \land \neg y \in ⋃_{x \in A} C)$
9	1 4 8	3bitr3g	$⊢ A \neq \emptyset \to (\forall x \in A y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in ⋃_{x \in A} C))$
10		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C))$
11	10	elv	$⊢ y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C)$
12		eldif	$⊢ y \in (B ∖ ⋃_{x \in A} C) \leftrightarrow (y \in B \land \neg y \in ⋃_{x \in A} C)$
13	9 11 12	3bitr4g	$⊢ A \neq \emptyset \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow y \in (B ∖ ⋃_{x \in A} C))$
14	13	eqrdv	$⊢ A \neq \emptyset \to ⋂_{x \in A} (B ∖ C) = B ∖ ⋃_{x \in A} C$