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