Theorem riotacl 5916

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 3278	. 2 |- { x e. A | ph } C_ A
2		riotacl2 5915	. 2 |- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
3	1, 2	sselid 3191	1 |- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )

Syntax hints:   -> wi 4   e. wcel 2176   E!wreu 2486   {crab 2488   iota_crio 5900

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-uni 3851  df-iota 5233  df-riota 5901

This theorem is referenced by:  riotaprop  5925  riotass2  5928  riotass  5929  acexmidlemcase  5941  supclti  7102  caucvgsrlemcl  7904  caucvgsrlemgt1  7910  axcaucvglemcl  8010  subval  8266  subcl  8273  divvalap  8749  divclap  8753  lbcl  9021  divfnzn  9744  flqcl  10418  flapcl  10420  cjval  11189  cjth  11190  cjf  11191  oddpwdclemodd  12527  oddpwdclemdc  12528  oddpwdc  12529  qnumdencl  12542  qnumdenbi  12547  ismgmid  13242  grpinvf  13412