This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-nul

Description: The Null Set Axiom of ZF set theory. It was derived as axnul 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)

		Ref	Expression
	Assertion	ax-nul	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		vy	⊢ 𝑦
2	1	cv	⊢ 𝑦
3	0	cv	⊢ 𝑥
4	2 3	wcel	⊢ 𝑦 ∈ 𝑥
5	4	wn	⊢ ¬ 𝑦 ∈ 𝑥
6	5 1	wal	⊢ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥
7	6 0	wex	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥