Metamath Proof Explorer


Theorem riota1

Description: Property of restricted iota. Compare iota1 . (Contributed by Mario Carneiro, 15-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 df-reu ∃! x A φ ∃! x x A φ
2 iota1 ∃! x x A φ x A φ ι x | x A φ = x
3 1 2 sylbi ∃! x A φ x A φ ι x | x A φ = x
4 df-riota ι x A | φ = ι x | x A φ
5 4 eqeq1i ι x A | φ = x ι x | x A φ = x
6 3 5 bitr4di ∃! x A φ x A φ ι x A | φ = x