MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riotacl Structured version   Unicode version

Theorem riotacl 6172
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
StepHypRef Expression
1 ssrab2 3499 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6171 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3415 1  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   E!wreu 2734   {crab 2736   iota_crio 6157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-un 3394  df-in 3396  df-ss 3403  df-sn 3945  df-pr 3947  df-uni 4164  df-iota 5460  df-riota 6158
This theorem is referenced by:  riotaprop  6181  riotass2  6184  riotass  6185  riotaxfrd  6188  riotaclb  6195  supcl  7832  fisupcl  7842  htalem  8227  dfac8clem  8326  dfac2a  8423  fin23lem22  8620  zorn2lem1  8789  subcl  9732  divcl  10130  lbcl  10410  flcl  11831  cjf  12939  sqrtcl  13196  qnumdencl  14274  qnumdenbi  14279  catidcl  15089  lubcl  15732  glbcl  15745  ismgmid  16008  grpinvf  16211  pj1f  16832  mirf  24161  midf  24262  ismidb  24264  lmif  24271  islmib  24273  usgraidx2vlem1  24512  nbgraf1olem2  24563  frgrancvvdeqlem5  25155  grpoidcl  25336  grpoinvcl  25345  iorlid  25447  pjpreeq  26433  cnlnadjlem3  27104  adjbdln  27118  xdivcld  27772  cvmlift3lem3  28955  transportcl  29836  fourierdlem50  32105  usgedgvadf1lem1  32731  usgedgvadf1ALTlem1  32734  riotaclbgBAD  35098  lshpkrlem2  35249  lshpkrcl  35254  cdleme25cl  36496  cdleme29cl  36516  cdlemefrs29clN  36538  cdlemk29-3  37050  cdlemkid5  37074  dihlsscpre  37374  mapdhcl  37867  hdmapcl  37973  hgmapcl  38032
  Copyright terms: Public domain W3C validator