Axiom ax-nul 2715

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 2714 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily.

Assertion

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

Distinct variable group:   x,y

Detailed syntax breakdown of Axiom ax-nul

Step	Hyp	Ref	Expression
1		vy	. . . . . 6 set y
2	1	cv 957	. . . . 5 class y
3		vx	. . . . . 6 set x
4	3	cv 957	. . . . 5 class x
5	2, 4	wcel 960	. . . 4 wff y e. x
6	5	wn 2	. . 3 wff -. y e. x
7	6, 1	wal 956	. 2 wff A.y -. y e. x
8	7, 3	wex 982	1 wff E.xA.y -. y e. x

This axiom is referenced by:  0ex 2716  dtruALT 2754

Copyright terms: Public domain