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	|- E. x A. y -. y e. x

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2	1	cv	|- y
3	0	cv	|- x
4	2 3	wcel	|- y e. x
5	4	wn	|- -. y e. x
6	5 1	wal	|- A. y -. y e. x
7	6 0	wex	|- E. x A. y -. y e. x