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 ) )