Axiom ax-nul 2705

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 2704 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	⊢ ∃x∀y ¬ y ∈ 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 953	. . . . 5 class y
3		vx	. . . . . 6 set x
4	3	cv 953	. . . . 5 class x
5	2, 4	wcel 956	. . . 4 wff y ∈ x
6	5	wn 2	. . 3 wff ¬ y ∈ x
7	6, 1	wal 952	. 2 wff ∀y ¬ y ∈ x
8	7, 3	wex 978	1 wff ∃x∀y ¬ y ∈ x

This axiom is referenced by:  0ex 2706  dtruALT 2743

Copyright terms: Public domain