Metamath Proof Explorer


Theorem riota1

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

Ref Expression
Assertion riota1
|- ( E! x e. A ph -> ( ( x e. A /\ ph ) <-> ( iota_ x e. A ph ) = x ) )

Proof

Step Hyp Ref Expression
1 df-reu
 |-  ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
2 iota1
 |-  ( E! x ( x e. A /\ ph ) -> ( ( x e. A /\ ph ) <-> ( iota x ( x e. A /\ ph ) ) = x ) )
3 1 2 sylbi
 |-  ( E! x e. A ph -> ( ( x e. A /\ ph ) <-> ( iota x ( x e. A /\ ph ) ) = x ) )
4 df-riota
 |-  ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) )
5 4 eqeq1i
 |-  ( ( iota_ x e. A ph ) = x <-> ( iota x ( x e. A /\ ph ) ) = x )
6 3 5 bitr4di
 |-  ( E! x e. A ph -> ( ( x e. A /\ ph ) <-> ( iota_ x e. A ph ) = x ) )