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	$$⊢\varnothing \in M\to \exists x\in M\forall y\in M\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg y\in \varnothing$$
2	1	rgenw	$$⊢\forall y\in M\neg y\in \varnothing$$
3		eleq2	$$⊢x=\varnothing \to \left(y\in x\leftrightarrow y\in \varnothing \right)$$
4	3	notbid	$$⊢x=\varnothing \to \left(\neg y\in x\leftrightarrow \neg y\in \varnothing \right)$$
5	4	ralbidv	$$⊢x=\varnothing \to \left(\forall y\in M\neg y\in x\leftrightarrow \forall y\in M\neg y\in \varnothing \right)$$
6	5	rspcev	$$⊢\left(\varnothing \in M\wedge \forall y\in M\neg y\in \varnothing \right)\to \exists x\in M\forall y\in M\neg y\in x$$
7	2 6	mpan2	$$⊢\varnothing \in M\to \exists x\in M\forall y\in M\neg y\in x$$