Axiom ax-nul 3645

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 3644 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 1614	. . . . 5 class y
3		vx	. . . . . 6 set x
4	3	cv 1614	. . . . 5 class x
5	2, 4	wcel 1617	. . . 4 wff y e. x
6	5	wn 2	. . 3 wff -. y e. x
7	6, 1	wal 1613	. 2 wff A.y -. y e. x
8	7, 3	wex 1644	1 wff E.xA.y -. y e. x

This axiom is referenced by:  0ex 3646  dtru 3694

Copyright terms: Public domain