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
|- ( iota x A. y y e. x ) = (/)

Proof

Step Hyp Ref Expression
1 nalset
 |-  -. E. x A. y y e. x
2 1 intnanr
 |-  -. ( E. x A. y y e. x /\ E* x A. y y e. x )
3 df-eu
 |-  ( E! x A. y y e. x <-> ( E. x A. y y e. x /\ E* x A. y y e. x ) )
4 2 3 mtbir
 |-  -. E! x A. y y e. x
5 iotanul
 |-  ( -. E! x A. y y e. x -> ( iota x A. y y e. x ) = (/) )
6 4 5 ax-mp
 |-  ( iota x A. y y e. x ) = (/)