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	⊢ ( ∅ ∈ 𝑀 → ∃ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑦 ∈ ∅
2	1	rgenw	⊢ ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ ∅
3		eleq2	⊢ ( 𝑥 = ∅ → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ∅ ) )
4	3	notbid	⊢ ( 𝑥 = ∅ → ( ¬ 𝑦 ∈ 𝑥 ↔ ¬ 𝑦 ∈ ∅ ) )
5	4	ralbidv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ ∅ ) )
6	5	rspcev	⊢ ( ( ∅ ∈ 𝑀 ∧ ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ ∅ ) → ∃ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥 )
7	2 6	mpan2	⊢ ( ∅ ∈ 𝑀 → ∃ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥 )