Metamath Proof Explorer

Theorem 0elaxnul

Description: A class that contains the empty set models the Null Set Axiom ax-nul . (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion 0elaxnul ⊢ ∅ ∈ M → ∃ x ∈ M ∀ y ∈ M ¬ y ∈ x

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ y ∈ ∅
2 1 rgenw ⊢ ∀ y ∈ M ¬ y ∈ ∅
3 eleq2 ⊢ x = ∅ → y ∈ x ↔ y ∈ ∅
4 3 notbid ⊢ x = ∅ → ¬ y ∈ x ↔ ¬ y ∈ ∅
5 4 ralbidv ⊢ x = ∅ → ∀ y ∈ M ¬ y ∈ x ↔ ∀ y ∈ M ¬ y ∈ ∅
6 5 rspcev ⊢ ∅ ∈ M ∧ ∀ y ∈ M ¬ y ∈ ∅ → ∃ x ∈ M ∀ y ∈ M ¬ y ∈ x
7 2 6 mpan2 ⊢ ∅ ∈ M → ∃ x ∈ M ∀ y ∈ M ¬ y ∈ x