Theorem riotacl 5844

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 3240	. 2 |- { x e. A | ph } C_ A
2		riotacl2 5843	. 2 |- ( E! x e. A ph -> ( iota_ x e. A ph ) e. { x e. A | ph } )
3	1, 2	sselid 3153	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 5829

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 2739  df-sbc 2963  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-uni 3810  df-iota 5178  df-riota 5830

This theorem is referenced by:  riotaprop  5853  riotass2  5856  riotass  5857  acexmidlemcase  5869  supclti  6996  caucvgsrlemcl  7787  caucvgsrlemgt1  7793  axcaucvglemcl  7893  subval  8148  subcl  8155  divvalap  8630  divclap  8634  lbcl  8902  divfnzn  9620  flqcl  10272  flapcl  10274  cjval  10853  cjth  10854  cjf  10855  oddpwdclemodd  12171  oddpwdclemdc  12172  oddpwdc  12173  qnumdencl  12186  qnumdenbi  12191  ismgmid  12795  grpinvf  12919