Theorem iun0

Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg y\in \varnothing$$
2	1	a1i	$$⊢x\in A\to \neg y\in \varnothing$$
3	2	nrex	$$⊢\neg \exists x\in Ay\in \varnothing$$
4		eliun	$$⊢y\in \bigcup _{x\in A}\varnothing \leftrightarrow \exists x\in Ay\in \varnothing$$
5	3 4	mtbir	$$⊢\neg y\in \bigcup _{x\in A}\varnothing$$
6	5	nel0	$$⊢\bigcup _{x\in A}\varnothing =\varnothing$$