Theorem wfaxnul

Description: The class of well-founded sets models the Null Set Axiom ax-nul . (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
Assertion	wfaxnul	$$⊢\exists x\in W\forall y\in W\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		wfax.1	$$⊢W=\bigcup R_1\left[\mathrm{On}\right]$$
2		onwf	$$⊢\mathrm{On}\subseteq \bigcup R_1\left[\mathrm{On}\right]$$
3		0elon	$$⊢\varnothing \in \mathrm{On}$$
4	2 3	sselii	$$⊢\varnothing \in \bigcup R_1\left[\mathrm{On}\right]$$
5	4 1	eleqtrri	$$⊢\varnothing \in W$$
6		0elaxnul	$$⊢\varnothing \in W\to \exists x\in W\forall y\in W\neg y\in x$$
7	5 6	ax-mp	$$⊢\exists x\in W\forall y\in W\neg y\in x$$