Theorem riotacl 5845

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

Syntax hints:   -> wi 4   e. wcel 2148   E!wreu 2457   {crab 2459   iota_crio 5830

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-un 3134  df-in 3136  df-ss 3143  df-sn 3599  df-pr 3600  df-uni 3811  df-iota 5179  df-riota 5831

This theorem is referenced by:  riotaprop  5854  riotass2  5857  riotass  5858  acexmidlemcase  5870  supclti  6997  caucvgsrlemcl  7788  caucvgsrlemgt1  7794  axcaucvglemcl  7894  subval  8149  subcl  8156  divvalap  8631  divclap  8635  lbcl  8903  divfnzn  9621  flqcl  10273  flapcl  10275  cjval  10854  cjth  10855  cjf  10856  oddpwdclemodd  12172  oddpwdclemdc  12173  oddpwdc  12174  qnumdencl  12187  qnumdenbi  12192  ismgmid  12796  grpinvf  12920