iindif1

Description: Indexed intersection of class difference with the subtrahend held constant. (Contributed by Thierry Arnoux, 21-Aug-2023)

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

Step	Hyp	Ref	Expression
1		r19.27zv	$⊢ A \neq \emptyset \to (\forall x \in A (y \in B \land \neg y \in C) \leftrightarrow (\forall x \in A y \in B \land \neg y \in C))$
2		eldif	$⊢ y \in (B ∖ C) \leftrightarrow (y \in B \land \neg y \in C)$
3	2	ralbii	$⊢ \forall x \in A y \in (B ∖ C) \leftrightarrow \forall x \in A (y \in B \land \neg y \in C)$
4		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} B \leftrightarrow \forall x \in A y \in B)$
5	4	elv	$⊢ y \in ⋂_{x \in A} B \leftrightarrow \forall x \in A y \in B$
6	5	anbi1i	$⊢ (y \in ⋂_{x \in A} B \land \neg y \in C) \leftrightarrow (\forall x \in A y \in B \land \neg y \in C)$
7	1 3 6	3bitr4g	$⊢ A \neq \emptyset \to (\forall x \in A y \in (B ∖ C) \leftrightarrow (y \in ⋂_{x \in A} B \land \neg y \in C))$
8		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C))$
9	8	elv	$⊢ y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow \forall x \in A y \in (B ∖ C)$
10		eldif	$⊢ y \in (⋂_{x \in A} B ∖ C) \leftrightarrow (y \in ⋂_{x \in A} B \land \neg y \in C)$
11	7 9 10	3bitr4g	$⊢ A \neq \emptyset \to (y \in ⋂_{x \in A} (B ∖ C) \leftrightarrow y \in (⋂_{x \in A} B ∖ C))$
12	11	eqrdv	$⊢ A \neq \emptyset \to ⋂_{x \in A} (B ∖ C) = ⋂_{x \in A} B ∖ C$

Metamath Proof Explorer