Metamath Proof Explorer

Theorem iindif2f

Description: Indexed intersection of class difference. Generalization of half of theorem "De Morgan's laws". (Contributed by Glauco Siliprandi, 24-Jan-2025)

		Ref	Expression
	Hypotheses	iindif2f.1	$⊢ \underline{Ⅎ} x A$
		iindif2f.2	$⊢ \underline{Ⅎ} x B$
	Assertion	iindif2f	$⊢ A \neq \emptyset \to ⋂_{x \in A} (B ∖ C) = B ∖ ⋃_{x \in A} C$

Proof

Step	Hyp	Ref	Expression
1		iindif2f.1	$⊢ \underline{Ⅎ} x A$
2		iindif2f.2	$⊢ \underline{Ⅎ} x B$
3	2	nfcri	$⊢ Ⅎ x y \in B$
4	3 1	r19.28zf	$⊢ 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))$
5		eldif	$⊢ y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in C)$
6	5	bicomi	$⊢ (y \in B \land \neg y \in C) \leftrightarrow y \in (B ∖ C)$
7	6	ralbii	$⊢ \forall x \in A (y \in B \land \neg y \in C) \leftrightarrow \forall x \in A y \in (B ∖ C)$
8		ralnex	$⊢ \forall x \in A \neg y \in C \leftrightarrow \neg \exists x \in A y \in C$
9		eliun	$⊢ y \in ⋃_{x \in A} C \leftrightarrow \exists x \in A y \in C$
10	8 9	xchbinxr	$⊢ \forall x \in A \neg y \in C \leftrightarrow \neg y \in ⋃_{x \in A} C$
11	10	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)$
12	4 7 11	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))$
13		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C))$
14	13	elv	$⊢ y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C)$
15		eldif	$⊢ y \in (B ∖ ⋃_{x \in A} C) \leftrightarrow (y \in B \land \neg y \in ⋃_{x \in A} C)$
16	12 14 15	3bitr4g	$⊢ A \neq \emptyset \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow y \in (B ∖ ⋃_{x \in A} C))$
17	16	eqrdv	$⊢ A \neq \emptyset \to ⋂_{x \in A} (B ∖ C) = B ∖ ⋃_{x \in A} C$