Theorem 0iin

Description: An empty indexed intersection is the universal class. (Contributed by NM, 20-Oct-2005)

	Ref	Expression
Assertion	0iin	$$⊢\bigcap _{x\in \varnothing }A=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-iin	$$⊢\bigcap _{x\in \varnothing }A=\left\{y|\forall x\in \varnothing y\in A\right\}$$
2		vex	$$⊢y\in \mathrm{V}$$
3		ral0	$$⊢\forall x\in \varnothing y\in A$$
4	2 3	2th	$$⊢y\in \mathrm{V}\leftrightarrow \forall x\in \varnothing y\in A$$
5	4	eqabi	$$⊢\mathrm{V}=\left\{y|\forall x\in \varnothing y\in A\right\}$$
6	1 5	eqtr4i	$$⊢\bigcap _{x\in \varnothing }A=\mathrm{V}$$