Axiom ax-nul

Description: The Null Set Axiom of ZF set theory. It was derived as axnul above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 7-Aug-2003)

	Ref	Expression
Assertion	ax-nul	$$⊢\exists x\forall y\neg y\in x$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		vy	$$setvary$$
2	1	cv	$$setvary$$
3	0	cv	$$setvarx$$
4	2 3	wcel	$$wffy\in x$$
5	4	wn	$$wff\neg y\in x$$
6	5 1	wal	$$wff\forall y\neg y\in x$$
7	6 0	wex	$$wff\exists x\forall y\neg y\in x$$