Theorem riotacl 5970

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

Syntax hints:   -> wi 4   e. wcel 2200   E!wreu 2510   {crab 2512   iota_crio 5953

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-uni 3889  df-iota 5278  df-riota 5954

This theorem is referenced by:  riotaeqimp  5979  riotaprop  5980  riotass2  5983  riotass  5984  acexmidlemcase  5996  supclti  7165  caucvgsrlemcl  7976  caucvgsrlemgt1  7982  axcaucvglemcl  8082  subval  8338  subcl  8345  divvalap  8821  divclap  8825  lbcl  9093  divfnzn  9816  flqcl  10493  flapcl  10495  cjval  11356  cjth  11357  cjf  11358  oddpwdclemodd  12694  oddpwdclemdc  12695  oddpwdc  12696  qnumdencl  12709  qnumdenbi  12714  ismgmid  13410  grpinvf  13580  uspgredg2vlem  16018  usgredg2vlem1  16020