Theorem riotacl 5583

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 3095	. 2 |- { x e. A | ph } C_ A
2		riotacl2 5582	. 2 |- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
3	1, 2	sseldi 3012	1 |- ( E! x e. A ph -> ( iota_ x e. A ph ) e. A )

Syntax hints:   -> wi 4   e. wcel 1436   E!wreu 2357   {crab 2359   iota_crio 5568

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-eu 1948  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-reu 2362  df-rab 2364  df-v 2617  df-sbc 2830  df-un 2992  df-in 2994  df-ss 3001  df-sn 3437  df-pr 3438  df-uni 3637  df-iota 4946  df-riota 5569

This theorem is referenced by:  riotaprop  5592  riotass2  5595  riotass  5596  acexmidlemcase  5608  supclti  6637  caucvgsrlemcl  7278  caucvgsrlemgt1  7284  axcaucvglemcl  7374  subval  7618  subcl  7625  divvalap  8080  divclap  8084  lbcl  8342  divfnzn  9038  flqcl  9608  flapcl  9610  cjval  10175  cjth  10176  cjf  10177  oddpwdclemodd  11032  oddpwdclemdc  11033  oddpwdc  11034  qnumdencl  11047  qnumdenbi  11052