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

Theorem riotacl 6280
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 3548 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6279 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3464 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 1869   E!wreu 2778   {crab 2780   iota_crio 6265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3302  df-un 3443  df-in 3445  df-ss 3452  df-sn 3999  df-pr 4001  df-uni 4219  df-iota 5564  df-riota 6266
This theorem is referenced by:  riotaprop  6289  riotass2  6292  riotass  6293  riotaxfrd  6296  riotaclb  6303  supcl  7980  fisupcl  7993  htalem  8374  dfac8clem  8469  dfac2a  8566  fin23lem22  8763  zorn2lem1  8932  subcl  9880  divcl  10282  lbcl  10563  flcl  12036  cjf  13165  sqrtcl  13422  qnumdencl  14685  qnumdenbi  14690  catidcl  15585  lubcl  16228  glbcl  16241  ismgmid  16504  grpinvf  16707  pj1f  17344  mirf  24701  midf  24814  ismidb  24816  lmif  24823  islmib  24825  usgraidx2vlem1  25114  nbgraf1olem2  25166  frgrancvvdeqlem5  25758  grpoidcl  25941  grpoinvcl  25950  iorlid  26052  pjpreeq  27047  cnlnadjlem3  27718  adjbdln  27732  xdivcld  28397  cvmlift3lem3  30050  transportcl  30803  finxpreclem4  31748  poimirlem26  31928  riotaclbgBAD  32493  lshpkrlem2  32644  lshpkrcl  32649  cdleme25cl  33891  cdleme29cl  33911  cdlemefrs29clN  33933  cdlemk29-3  34445  cdlemkid5  34469  dihlsscpre  34769  mapdhcl  35262  hdmapcl  35368  hgmapcl  35427  wessf1ornlem  37357  fourierdlem50  37888  usgridx2vlem1  38973  usgedgvadf1lem1  39117  usgedgvadf1ALTlem1  39120
  Copyright terms: Public domain W3C validator