This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$setvar x$
1		vy	$setvar y$
2	1	cv	$setvar y$
3	0	cv	$setvar x$
4	2 3	wcel	$wff y \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$