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 = U. ( R1 " On )
Assertion	wfaxnul	|- E. x e. W A. y e. W -. y e. x

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		onwf	|- On C_ U. ( R1 " On )
3		0elon	|- (/) e. On
4	2 3	sselii	|- (/) e. U. ( R1 " On )
5	4 1	eleqtrri	|- (/) e. W
6		0elaxnul	|- ( (/) e. W -> E. x e. W A. y e. W -. y e. x )
7	5 6	ax-mp	|- E. x e. W A. y e. W -. y e. x