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

Theorem riotacl 6086
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 3456 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6085 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3373 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 1756   E!wreu 2736   {crab 2738   iota_crio 6070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2740  df-reu 2741  df-rab 2743  df-v 2993  df-sbc 3206  df-un 3352  df-in 3354  df-ss 3361  df-sn 3897  df-pr 3899  df-uni 4111  df-iota 5400  df-riota 6071
This theorem is referenced by:  riotaprop  6095  riotass2  6098  riotass  6099  riotaxfrd  6102  riotaclb  6109  supcl  7727  fisupcl  7736  htalem  8122  dfac8clem  8221  dfac2a  8318  fin23lem22  8515  zorn2lem1  8684  subcl  9628  divcl  10019  lbcl  10300  flcl  11664  cjf  12612  sqrcl  12868  qnumdencl  13836  qnumdenbi  13841  catidcl  14639  lubcl  15174  glbcl  15187  ismgmid  15454  grpinvf  15601  pj1f  16213  mirf  23083  usgraidx2vlem1  23328  nbgraf1olem2  23370  grpoidcl  23723  grpoinvcl  23732  iorlid  23834  pjpreeq  24820  cnlnadjlem3  25492  adjbdln  25506  xdivcld  26117  cvmlift3lem3  27229  transportcl  28083  frgrancvvdeqlem5  30650  riotaclbgBAD  32628  riotaclbBAD  32629  lshpkrlem2  32779  lshpkrcl  32784  cdleme25cl  34024  cdleme29cl  34044  cdlemefrs29clN  34066  cdlemk29-3  34578  cdlemkid5  34602  dihlsscpre  34902  mapdhcl  35395  hdmapcl  35501  hgmapcl  35560
  Copyright terms: Public domain W3C validator