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

Theorem riotacl 6593
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 3414 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6592 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3332 1  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  e.  A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1727   E!wreu 2713   {crab 2715   iota_crio 6571
This theorem is referenced by:  riotaprop  6602  riotass2  6606  riotass  6607  riotaxfrd  6610  riotaclbg  6618  riotaundb  6620  supcl  7492  fisupcl  7501  htalem  7851  dfac8clem  7944  dfac2a  8041  fin23lem22  8238  zorn2lem1  8407  subcl  9336  divcl  9715  lbcl  9990  flcl  11235  cjf  11940  sqrcl  12196  qnumdencl  13162  qnumdenbi  13167  catidcl  13938  ismgmid  14741  grpinvf  14880  pj1f  15360  usgraidx2vlem1  21441  nbgraf1olem2  21483  grpoidcl  21836  grpoinvcl  21845  iorlid  21947  pjpreeq  22931  cnlnadjlem3  23603  adjbdln  23617  xdivcld  24200  cvmlift3lem3  25039  transportcl  25998  frgrancvvdeqlem5  28521  lshpkrlem2  30007  lshpkrcl  30012  dihlsscpre  32130  mapdhcl  32623  hdmapcl  32729  hgmapcl  32788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-rex 2717  df-reu 2718  df-rab 2720  df-v 2964  df-sbc 3168  df-un 3311  df-in 3313  df-ss 3320  df-if 3764  df-sn 3844  df-pr 3845  df-uni 4040  df-iota 5447  df-riota 6578
  Copyright terms: Public domain W3C validator