Theorem 0iun

Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	0iun	$$⊢\bigcup _{x\in \varnothing }A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rex0	$$⊢\neg \exists x\in \varnothing y\in A$$
2		eliun	$$⊢y\in \bigcup _{x\in \varnothing }A\leftrightarrow \exists x\in \varnothing y\in A$$
3	1 2	mtbir	$$⊢\neg y\in \bigcup _{x\in \varnothing }A$$
4	3	nel0	$$⊢\bigcup _{x\in \varnothing }A=\varnothing$$