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 x y ¬ y x

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 vy setvar y
2 1 cv setvar y
3 0 cv setvar x
4 2 3 wcel wff y x
5 4 wn wff ¬ y x
6 5 1 wal wff y ¬ y x
7 6 0 wex wff x y ¬ y x