Theorem bj-nul

Description: Two formulations of the axiom of the empty set ax-nul . Proposal: place it right before ax-nul . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nul	$$⊢\varnothing \in \mathrm{V}\leftrightarrow \exists x\forall y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		isset	$$⊢\varnothing \in \mathrm{V}\leftrightarrow \exists xx=\varnothing$$
2		eq0	$$⊢x=\varnothing \leftrightarrow \forall y\neg y\in x$$
3	2	exbii	$$⊢\exists xx=\varnothing \leftrightarrow \exists x\forall y\neg y\in x$$
4	1 3	bitri	$$⊢\varnothing \in \mathrm{V}\leftrightarrow \exists x\forall y\neg y\in x$$