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 
|- E. x A. y -. y e. x

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 
 |-  x
1 vy 
 |-  y
2 1 cv 
 |-  y
3 0 cv 
 |-  x
4 2 3 wcel 
 |-  y e. x
5 4 wn 
 |-  -. y e. x
6 5 1 wal 
 |-  A. y -. y e. x
7 6 0 wex 
 |-  E. x A. y -. y e. x