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 = ∅

Proof

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 = ∅