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

Theorem riotacl 6271
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 3590 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6270 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3507 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 1767   E!wreu 2819   {crab 2821   iota_crio 6255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2823  df-reu 2824  df-rab 2826  df-v 3120  df-sbc 3337  df-un 3486  df-in 3488  df-ss 3495  df-sn 4034  df-pr 4036  df-uni 4252  df-iota 5557  df-riota 6256
This theorem is referenced by:  riotaprop  6280  riotass2  6283  riotass  6284  riotaxfrd  6287  riotaclb  6294  supcl  7930  fisupcl  7939  htalem  8326  dfac8clem  8425  dfac2a  8522  fin23lem22  8719  zorn2lem1  8888  subcl  9831  divcl  10225  lbcl  10506  flcl  11912  cjf  12917  sqrtcl  13174  qnumdencl  14148  qnumdenbi  14153  catidcl  14954  lubcl  15489  glbcl  15502  ismgmid  15765  grpinvf  15966  pj1f  16588  mirf  23893  midf  23966  ismidb  23968  lmif  23975  islmib  23977  usgraidx2vlem1  24214  nbgraf1olem2  24265  frgrancvvdeqlem5  24858  grpoidcl  25042  grpoinvcl  25051  iorlid  25153  pjpreeq  26139  cnlnadjlem3  26811  adjbdln  26825  xdivcld  27443  cvmlift3lem3  28591  transportcl  29610  fourierdlem50  31780  usgedgvadf1lem1  32203  usgedgvadf1ALTlem1  32206  riotaclbgBAD  34158  riotaclbBAD  34159  lshpkrlem2  34309  lshpkrcl  34314  cdleme25cl  35554  cdleme29cl  35574  cdlemefrs29clN  35596  cdlemk29-3  36108  cdlemkid5  36132  dihlsscpre  36432  mapdhcl  36925  hdmapcl  37031  hgmapcl  37090
  Copyright terms: Public domain W3C validator