Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > axnul  Unicode version 
Description: The Null Set Axiom of ZF set theory. It was derived as axnul 4164 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 1697  . . . 4 
4  3  wn 3  . . 3 
5  4, 1  wal 1530  . 2 
6  5, 2  wex 1531  1 
Colors of variables: wff set class 
This axiom is referenced by: 0ex 4166 dtru 4217 
Copyright terms: Public domain  W3C validator 