Metamath Proof Explorer


Theorem riota1a

Description: Property of iota. (Contributed by NM, 23-Aug-2011)

Ref Expression
Assertion riota1a x A ∃! x A φ φ ι x | x A φ = x

Proof

Step Hyp Ref Expression
1 ibar x A φ x A φ
2 df-reu ∃! x A φ ∃! x x A φ
3 iota1 ∃! x x A φ x A φ ι x | x A φ = x
4 2 3 sylbi ∃! x A φ x A φ ι x | x A φ = x
5 1 4 sylan9bb x A ∃! x A φ φ ι x | x A φ = x