Theorem bj-nuliota

Description: Definition of the empty set using the definite description binder. See also bj-nuliotaALT . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nuliota	⊢ ∅ = ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	eueqi	⊢ ∃! 𝑥 𝑥 = ∅
3		eq0	⊢ ( 𝑥 = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
4	3	eubii	⊢ ( ∃! 𝑥 𝑥 = ∅ ↔ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )
5	2 4	mpbi	⊢ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥
6		eleq2	⊢ ( 𝑥 = ∅ → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ∅ ) )
7	6	notbid	⊢ ( 𝑥 = ∅ → ( ¬ 𝑦 ∈ 𝑥 ↔ ¬ 𝑦 ∈ ∅ ) )
8	7	albidv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ¬ 𝑦 ∈ ∅ ) )
9	8	iota2	⊢ ( ( ∅ ∈ V ∧ ∃! 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) → ( ∀ 𝑦 ¬ 𝑦 ∈ ∅ ↔ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) = ∅ ) )
10	1 5 9	mp2an	⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ ∅ ↔ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) = ∅ )
11		noel	⊢ ¬ 𝑦 ∈ ∅
12	10 11	mpgbi	⊢ ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 ) = ∅
13	12	eqcomi	⊢ ∅ = ( ℩ 𝑥 ∀ 𝑦 ¬ 𝑦 ∈ 𝑥 )