Metamath Proof Explorer

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 ⊢ ι x | ∀ y y ∈ x = ∅

Proof

Step Hyp Ref Expression
1 nalset ⊢ ¬ ∃ x ∀ y y ∈ x
2 1 intnanr ⊢ ¬ ∃ x ∀ y y ∈ x ∧ ∃* x ∀ y y ∈ x
3 df-eu ⊢ ∃! x ∀ y y ∈ x ↔ ∃ x ∀ y y ∈ x ∧ ∃* x ∀ y y ∈ x
4 2 3 mtbir ⊢ ¬ ∃! x ∀ y y ∈ x
5 iotanul ⊢ ¬ ∃! x ∀ y y ∈ x → ι x | ∀ y y ∈ x = ∅
6 4 5 ax-mp ⊢ ι x | ∀ y y ∈ x = ∅