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	|- ( (/) e. M -> E. x e. M A. y e. M -. y e. x )

Proof

Step	Hyp	Ref	Expression
1		noel	|- -. y e. (/)
2	1	rgenw	|- A. y e. M -. y e. (/)
3		eleq2	|- ( x = (/) -> ( y e. x <-> y e. (/) ) )
4	3	notbid	|- ( x = (/) -> ( -. y e. x <-> -. y e. (/) ) )
5	4	ralbidv	|- ( x = (/) -> ( A. y e. M -. y e. x <-> A. y e. M -. y e. (/) ) )
6	5	rspcev	|- ( ( (/) e. M /\ A. y e. M -. y e. (/) ) -> E. x e. M A. y e. M -. y e. x )
7	2 6	mpan2	|- ( (/) e. M -> E. x e. M A. y e. M -. y e. x )