Metamath Proof Explorer

Theorem aiota0def

Description: Example for a defined alternate 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). This corresponds to iota0def . (Contributed by AV, 25-Aug-2022)

Ref Expression
Assertion aiota0def ⊢ ι = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 al0ssb ⊢ ∀ y x ⊆ y ↔ x = ∅
3 2 ax-gen ⊢ ∀ x ∀ y x ⊆ y ↔ x = ∅
4 eqeq2 ⊢ z = ∅ → x = z ↔ x = ∅
5 4 bibi2d ⊢ z = ∅ → ∀ y x ⊆ y ↔ x = z ↔ ∀ y x ⊆ y ↔ x = ∅
6 5 albidv ⊢ z = ∅ → ∀ x ∀ y x ⊆ y ↔ x = z ↔ ∀ x ∀ y x ⊆ y ↔ x = ∅
7 eqeq2 ⊢ z = ∅ → ι = z ↔ ι = ∅
8 6 7 imbi12d ⊢ z = ∅ → ∀ x ∀ y x ⊆ y ↔ x = z → ι = z ↔ ∀ x ∀ y x ⊆ y ↔ x = ∅ → ι = ∅
9 aiotaval ⊢ ∀ x ∀ y x ⊆ y ↔ x = z → ι = z
10 8 9 vtoclg ⊢ ∅ ∈ V → ∀ x ∀ y x ⊆ y ↔ x = ∅ → ι = ∅
11 1 3 10 mp2 ⊢ ι = ∅