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	⊢ ( ∅ ∈ V ↔ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		isset	⊢ ( ∅ ∈ V ↔ ∃ 𝑥 𝑥 = ∅ )
2		eq0	⊢ ( 𝑥 = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
3	2	exbii	⊢ ( ∃ 𝑥 𝑥 = ∅ ↔ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
4	1 3	bitri	⊢ ( ∅ ∈ V ↔ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )