Theorem riotacl 5866

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

Assertion

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

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem riotacl

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

Syntax hints:   -> wi 4   e. wcel 2160   E!wreu 2470   {crab 2472   iota_crio 5851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-un 3148  df-in 3150  df-ss 3157  df-sn 3613  df-pr 3614  df-uni 3825  df-iota 5196  df-riota 5852

This theorem is referenced by:  riotaprop  5875  riotass2  5878  riotass  5879  acexmidlemcase  5891  supclti  7027  caucvgsrlemcl  7818  caucvgsrlemgt1  7824  axcaucvglemcl  7924  subval  8179  subcl  8186  divvalap  8661  divclap  8665  lbcl  8933  divfnzn  9651  flqcl  10304  flapcl  10306  cjval  10886  cjth  10887  cjf  10888  oddpwdclemodd  12204  oddpwdclemdc  12205  oddpwdc  12206  qnumdencl  12219  qnumdenbi  12224  ismgmid  12853  grpinvf  12991