Theorem bj-axnul

Description: Over the base theory ax-1 -- ax-5 plus the axiom of separation (the universal closure of ax-sep ), simulated here by its instance with F. substituted for ph as an antecedent, the existence axiom extru is equivalent to the existence of an empty set (which can be called "the" empty set once ax-ext is assumed). The present proof proves only one implication, but the reverse implication is straightforward (though not expressible in this closed form since it involves another instance of the existence axiom). This proof only uses an instance of the axiom of separation with a bounded formula, so is valid in CZF (see the corresponding section in the "Intuitionistic Logic Explorer" iset.mm). (Contributed by BJ, 8-Mar-2026) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-axnul	|- ( A. x E. y A. z ( z e. y <-> ( z e. x /\ F. ) ) -> ( E. x T. -> E. y A. z -. z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		biimp	|- ( ( z e. y <-> ( z e. x /\ F. ) ) -> ( z e. y -> ( z e. x /\ F. ) ) )
2		falimd	|- ( ( z e. x /\ F. ) -> ( z e. y -> F. ) )
3	1 2	syli	|- ( ( z e. y <-> ( z e. x /\ F. ) ) -> ( z e. y -> F. ) )
4		dfnot	|- ( -. z e. y <-> ( z e. y -> F. ) )
5	3 4	sylibr	|- ( ( z e. y <-> ( z e. x /\ F. ) ) -> -. z e. y )
6	5	alimi	|- ( A. z ( z e. y <-> ( z e. x /\ F. ) ) -> A. z -. z e. y )
7	6	eximi	|- ( E. y A. z ( z e. y <-> ( z e. x /\ F. ) ) -> E. y A. z -. z e. y )
8	7	alimi	|- ( A. x E. y A. z ( z e. y <-> ( z e. x /\ F. ) ) -> A. x E. y A. z -. z e. y )
9		bj-spvw	|- ( E. x T. -> ( A. x E. y A. z -. z e. y -> E. y A. z -. z e. y ) )
10	8 9	syl5com	|- ( A. x E. y A. z ( z e. y <-> ( z e. x /\ F. ) ) -> ( E. x T. -> E. y A. z -. z e. y ) )