Theorem eu0

Description: There is only one empty set. (Contributed by RP, 1-Oct-2023)

	Ref	Expression
Assertion	eu0	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝑥 ∈ ∅
2	1	ax-gen	⊢ ∀ 𝑥 ¬ 𝑥 ∈ ∅
3		ax-nul	⊢ ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥
4		nulmo	⊢ ∃* 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥
5		df-eu	⊢ ( ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ( ∃ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ∧ ∃* 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) )
6	3 4 5	mpbir2an	⊢ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥
7	2 6	pm3.2i	⊢ ( ∀ 𝑥 ¬ 𝑥 ∈ ∅ ∧ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )