Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axnul  Structured version Unicode version 
Description: The Null Set Axiom of ZF set theory. It was derived as axnul 4581 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, 7Aug2003.) 
Ref  Expression 

axnul 
Step  Hyp  Ref  Expression 

1  vy  . . . . 5  
2  vx  . . . . 5  
3  1, 2  wel 1768  . . . 4 
4  3  wn 3  . . 3 
5  4, 1  wal 1377  . 2 
6  5, 2  wex 1596  1 
Colors of variables: wff setvar class 
This axiom is referenced by: 0ex 4583 dtru 4644 bjdtru 33865 
Copyright terms: Public domain  W3C validator 