Theorem riotacl 5914

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 5913	. 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 5898

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 5232  df-riota 5899

This theorem is referenced by:  riotaprop  5923  riotass2  5926  riotass  5927  acexmidlemcase  5939  supclti  7100  caucvgsrlemcl  7902  caucvgsrlemgt1  7908  axcaucvglemcl  8008  subval  8264  subcl  8271  divvalap  8747  divclap  8751  lbcl  9019  divfnzn  9742  flqcl  10416  flapcl  10418  cjval  11156  cjth  11157  cjf  11158  oddpwdclemodd  12494  oddpwdclemdc  12495  oddpwdc  12496  qnumdencl  12509  qnumdenbi  12514  ismgmid  13209  grpinvf  13379