iundif1

Description: Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018)

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

Step	Hyp	Ref	Expression
1		r19.41v	$⊢ \exists x \in A (y \in B \land \neg y \in C) \leftrightarrow (\exists 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	rexbii	$⊢ \exists x \in A y \in (B ∖ C) \leftrightarrow \exists x \in A (y \in B \land \neg y \in C)$
4		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
5	4	anbi1i	$⊢ (y \in ⋃_{x \in A} B \land \neg y \in C) \leftrightarrow (\exists x \in A y \in B \land \neg y \in C)$
6	1 3 5	3bitr4i	$⊢ \exists x \in A y \in (B ∖ C) \leftrightarrow (y \in ⋃_{x \in A} B \land \neg y \in C)$
7		eliun	$⊢ y \in ⋃_{x \in A} (B ∖ C) \leftrightarrow \exists x \in A y \in (B ∖ C)$
8		eldif	$⊢ y \in (⋃_{x \in A} B ∖ C) \leftrightarrow (y \in ⋃_{x \in A} B \land \neg y \in C)$
9	6 7 8	3bitr4i	$⊢ y \in ⋃_{x \in A} (B ∖ C) \leftrightarrow y \in (⋃_{x \in A} B ∖ C)$
10	9	eqriv	$⊢ ⋃_{x \in A} (B ∖ C) = ⋃_{x \in A} B ∖ C$

Metamath Proof Explorer