Theorem int0

Description: The intersection of the empty set is the universal class. Exercise 2 of TakeutiZaring p. 44. (Contributed by NM, 18-Aug-1993) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	int0	$$⊢\bigcap \varnothing =\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ral0	$$⊢\forall x\in \varnothing y\in x$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	elint2	$$⊢y\in \bigcap \varnothing \leftrightarrow \forall x\in \varnothing y\in x$$
4	1 3	mpbir	$$⊢y\in \bigcap \varnothing$$
5	4 2	2th	$$⊢y\in \bigcap \varnothing \leftrightarrow y\in \mathrm{V}$$
6	5	eqriv	$$⊢\bigcap \varnothing =\mathrm{V}$$