Theorem iunxdif3

Description: An indexed union where some terms are the empty set. See iunxdif2 . (Contributed by Thierry Arnoux, 4-May-2020)

	Ref	Expression
Hypothesis	iunxdif3.1	$$⊢\underset{\_}{Ⅎ}xE$$
Assertion	iunxdif3	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		iunxdif3.1	$$⊢\underset{\_}{Ⅎ}xE$$
2		inss2	$$⊢A\cap E\subseteq E$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4	3 1	nfin	$$⊢\underset{\_}{Ⅎ}x\left(A\cap E\right)$$
5	4 1	ssrexf	$$⊢A\cap E\subseteq E\to \left(\exists x\in \left(A\cap E\right)y\in B\to \exists x\in Ey\in B\right)$$
6		eliun	$$⊢y\in \bigcup _{x\in A\cap E}B\leftrightarrow \exists x\in \left(A\cap E\right)y\in B$$
7		eliun	$$⊢y\in \bigcup _{x\in E}B\leftrightarrow \exists x\in Ey\in B$$
8	5 6 7	3imtr4g	$$⊢A\cap E\subseteq E\to \left(y\in \bigcup _{x\in A\cap E}B\to y\in \bigcup _{x\in E}B\right)$$
9	8	ssrdv	$$⊢A\cap E\subseteq E\to \bigcup _{x\in A\cap E}B\subseteq \bigcup _{x\in E}B$$
10	2 9	ax-mp	$$⊢\bigcup _{x\in A\cap E}B\subseteq \bigcup _{x\in E}B$$
11		iuneq2	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in E}B=\bigcup _{x\in E}\varnothing$$
12		iun0	$$⊢\bigcup _{x\in E}\varnothing =\varnothing$$
13	11 12	eqtrdi	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in E}B=\varnothing$$
14	10 13	sseqtrid	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\cap E}B\subseteq \varnothing$$
15		ss0	$$⊢\bigcup _{x\in A\cap E}B\subseteq \varnothing \to \bigcup _{x\in A\cap E}B=\varnothing$$
16	14 15	syl	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\cap E}B=\varnothing$$
17	16	uneq1d	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\cap E}B\cup \bigcup _{x\in A\setminus E}B=\varnothing \cup \bigcup _{x\in A\setminus E}B$$
18		iunxun	$$⊢\bigcup _{x\in \left(A\cap E\right)\cup \left(A\setminus E\right)}B=\bigcup _{x\in A\cap E}B\cup \bigcup _{x\in A\setminus E}B$$
19		inundif	$$⊢\left(A\cap E\right)\cup \left(A\setminus E\right)=A$$
20	19	nfth	$$⊢Ⅎx\left(A\cap E\right)\cup \left(A\setminus E\right)=A$$
21	3 1	nfdif	$$⊢\underset{\_}{Ⅎ}x\left(A\setminus E\right)$$
22	4 21	nfun	$$⊢\underset{\_}{Ⅎ}x\left(\left(A\cap E\right)\cup \left(A\setminus E\right)\right)$$
23		id	$$⊢\left(A\cap E\right)\cup \left(A\setminus E\right)=A\to \left(A\cap E\right)\cup \left(A\setminus E\right)=A$$
24		eqidd	$$⊢\left(A\cap E\right)\cup \left(A\setminus E\right)=A\to B=B$$
25	20 22 3 23 24	iuneq12df	$$⊢\left(A\cap E\right)\cup \left(A\setminus E\right)=A\to \bigcup _{x\in \left(A\cap E\right)\cup \left(A\setminus E\right)}B=\bigcup _{x\in A}B$$
26	19 25	ax-mp	$$⊢\bigcup _{x\in \left(A\cap E\right)\cup \left(A\setminus E\right)}B=\bigcup _{x\in A}B$$
27	18 26	eqtr3i	$$⊢\bigcup _{x\in A\cap E}B\cup \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A}B$$
28	27	a1i	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\cap E}B\cup \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A}B$$
29		0un	$$⊢\varnothing \cup \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A\setminus E}B$$
30	29	a1i	$$⊢\forall x\in EB=\varnothing \to \varnothing \cup \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A\setminus E}B$$
31	17 28 30	3eqtr3rd	$$⊢\forall x\in EB=\varnothing \to \bigcup _{x\in A\setminus E}B=\bigcup _{x\in A}B$$