This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iota1

Description: Property of iota. (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion iota1 ⊢ ∃! x φ → φ ↔ ι x | φ = x

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ∃! x φ ↔ ∃ z ∀ x φ ↔ x = z
2 sp ⊢ ∀ x φ ↔ x = z → φ ↔ x = z
3 iotaval ⊢ ∀ x φ ↔ x = z → ι x | φ = z
4 3 eqeq2d ⊢ ∀ x φ ↔ x = z → x = ι x | φ ↔ x = z
5 2 4 bitr4d ⊢ ∀ x φ ↔ x = z → φ ↔ x = ι x | φ
6 eqcom ⊢ x = ι x | φ ↔ ι x | φ = x
7 5 6 bitrdi ⊢ ∀ x φ ↔ x = z → φ ↔ ι x | φ = x
8 7 exlimiv ⊢ ∃ z ∀ x φ ↔ x = z → φ ↔ ι x | φ = x
9 1 8 sylbi ⊢ ∃! x φ → φ ↔ ι x | φ = x