Theorem riotacl2

Description: Membership law for "the unique element in A such that ph ". (Contributed by NM, 21-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

	Ref	Expression
Assertion	riotacl2	|- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )

Proof

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