# Metamath Proof Explorer

## Theorem iota0def

Description: Example for a defined iota being the empty set, i.e., A. y x C_ y is a wff satisfied by a unique value x , namely x = (/) (the empty set is the one and only set which is a subset of every set). (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion iota0def ${⊢}\left(\iota {x}|\forall {y}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 al0ssb ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}↔{x}=\varnothing$
3 2 a1i ${⊢}\left(\varnothing \in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}↔{x}=\varnothing \right)$
4 3 iota5 ${⊢}\left(\varnothing \in \mathrm{V}\wedge \varnothing \in \mathrm{V}\right)\to \left(\iota {x}|\forall {y}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)=\varnothing$
5 1 1 4 mp2an ${⊢}\left(\iota {x}|\forall {y}\phantom{\rule{.4em}{0ex}}{x}\subseteq {y}\right)=\varnothing$