Theorem iunxdif2

Description: Indexed union with a class difference as its index. (Contributed by NM, 10-Dec-2004)

	Ref	Expression
Hypothesis	iunxdif2.1	$$⊢x=y\to C=D$$
Assertion	iunxdif2	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)C\subseteq D\to \bigcup _{y\in A\setminus B}D=\bigcup _{x\in A}C$$

Proof

Step	Hyp	Ref	Expression
1		iunxdif2.1	$$⊢x=y\to C=D$$
2		iunss2	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)C\subseteq D\to \bigcup _{x\in A}C\subseteq \bigcup _{y\in A\setminus B}D$$
3		difss	$$⊢A\setminus B\subseteq A$$
4		iunss1	$$⊢A\setminus B\subseteq A\to \bigcup _{y\in A\setminus B}D\subseteq \bigcup _{y\in A}D$$
5	3 4	ax-mp	$$⊢\bigcup _{y\in A\setminus B}D\subseteq \bigcup _{y\in A}D$$
6	1	cbviunv	$$⊢\bigcup _{x\in A}C=\bigcup _{y\in A}D$$
7	5 6	sseqtrri	$$⊢\bigcup _{y\in A\setminus B}D\subseteq \bigcup _{x\in A}C$$
8	2 7	jctil	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)C\subseteq D\to \left(\bigcup _{y\in A\setminus B}D\subseteq \bigcup _{x\in A}C\wedge \bigcup _{x\in A}C\subseteq \bigcup _{y\in A\setminus B}D\right)$$
9		eqss	$$⊢\bigcup _{y\in A\setminus B}D=\bigcup _{x\in A}C\leftrightarrow \left(\bigcup _{y\in A\setminus B}D\subseteq \bigcup _{x\in A}C\wedge \bigcup _{x\in A}C\subseteq \bigcup _{y\in A\setminus B}D\right)$$
10	8 9	sylibr	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)C\subseteq D\to \bigcup _{y\in A\setminus B}D=\bigcup _{x\in A}C$$