Axiom ax-nul 4115

Description: The Null Set Axiom of IZF set theory. It was derived as axnul 4114 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. Axiom 4 of [Crosilla] p. "Axioms of CZF and IZF". (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 2142	. . . 4 wff y e. x
4	3	wn 3	. . 3 wff -. y e. x
5	4, 1	wal 1346	. 2 wff A. y -. y e. x
6	5, 2	wex 1485	1 wff E. x A. y -. y e. x

This axiom is referenced by:  0ex  4116  dtruarb  4177