Theorem 0ex

Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of TakeutiZaring p. 20. For the unabbreviated version, see ax-nul . (Contributed by NM, 21-Jun-1993) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	0ex	$$⊢\varnothing \in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-nul	$$⊢\exists x\forall y\neg y\in x$$
2		eq0	$$⊢x=\varnothing \leftrightarrow \forall y\neg y\in x$$
3	2	exbii	$$⊢\exists xx=\varnothing \leftrightarrow \exists x\forall y\neg y\in x$$
4	1 3	mpbir	$$⊢\exists xx=\varnothing$$
5	4	issetri	$$⊢\varnothing \in \mathrm{V}$$