Axiom ax-nul 5268

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 5267 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	⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Axiom ax-nul

Step	Hyp	Ref	Expression
1		vy	. . . . 5 setvar 𝑦
2		vx	. . . . 5 setvar 𝑥
3	1, 2	wel 2142	. . . 4 wff 𝑦 ∈ 𝑥
4	3	wn 3	. . 3 wff ¬ 𝑦 ∈ 𝑥
5	4, 1	wal 1566	. 2 wff ∀𝑦 ¬ 𝑦 ∈ 𝑥
6	5, 2	wex 1807	1 wff ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥

This axiom is referenced by:  0ex  5269  dtruALT2  5341  axpr  5398  axprlem1OLD  5399  axprlem4OLD  5401  axprlem5OLD  5402  exexneq  5416  axsepg2  35519  axsepg3  35520  axsepg4  35522  axnulg  35524  axtcond  36955  eu0  44216