Theorem iota0ndef

Description: Example for an undefined iota being the empty set, i.e., A. y y e. x is a wff not satisfied by a (unique) value x (there is no set, and therefore certainly no unique set, which contains every set). (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	iota0ndef	⊢ ( ℩ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		nalset	⊢ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥
2	1	intnanr	⊢ ¬ ( ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ∧ ∃* 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 )
3		df-eu	⊢ ( ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ↔ ( ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ∧ ∃* 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) )
4	2 3	mtbir	⊢ ¬ ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥
5		iotanul	⊢ ( ¬ ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 → ( ℩ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) = ∅ )
6	4 5	ax-mp	⊢ ( ℩ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) = ∅