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 ι x | y x y =


Step Hyp Ref Expression
1 0ex V
2 al0ssb y x y x =
3 2 a1i V V y x y x =
4 3 iota5 V V ι x | y x y =
5 1 1 4 mp2an ι x | y x y =