Metamath Proof Explorer

Theorem riotacl

Description: Closure of restricted iota. (Contributed by NM, 21-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. A | ph } C_ A
2 riotacl2 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
3 1 2 sseldi 
 |-  ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )