Axiom ax-nul 4789

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 4788 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.)

Assertion

Ref	Expression
ax-nul	|- E. x A. y -. y e. x

Distinct variable group:   x, y

Detailed syntax breakdown of Axiom ax-nul

Step	Hyp	Ref	Expression
1		vy	. . . . 5 setvar y
2		vx	. . . . 5 setvar x
3	1, 2	wel 1991	. . . 4 wff y e. x
4	3	wn 3	. . 3 wff -. y e. x
5	4, 1	wal 1481	. 2 wff A. y -. y e. x
6	5, 2	wex 1704	1 wff E. x A. y -. y e. x

This axiom is referenced by:  0ex  4790  dtru  4857  bj-dtru  32797