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

Theorem riotacl 6319
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 3258 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6318 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3178 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 1684   E!wreu 2545   {crab 2547   iota_crio 6297
This theorem is referenced by:  riotaprop  6328  riotass2  6332  riotass  6333  riotaxfrd  6336  riotaclbg  6344  riotaundb  6346  supcl  7209  fisupcl  7218  htalem  7566  dfac8clem  7659  dfac2a  7756  fin23lem22  7953  zorn2lem1  8123  subcl  9051  divcl  9430  lbcl  9705  flcl  10927  cjf  11589  sqrcl  11845  qnumdencl  12810  qnumdenbi  12815  catidcl  13584  ismgmid  14387  grpinvf  14526  pj1f  15006  grpoidcl  20884  grpoinvcl  20893  iorlid  20995  pjpreeq  21977  cnlnadjlem3  22649  adjbdln  22663  xdivcld  23106  cvmlift3lem3  23852  transportcl  24656  lineval12  26081  lshpkrlem2  29301  lshpkrcl  29306  dihlsscpre  31424  mapdhcl  31917  hdmapcl  32023  hgmapcl  32082
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-un 3157  df-in 3159  df-ss 3166  df-if 3566  df-sn 3646  df-pr 3647  df-uni 3828  df-iota 5219  df-riota 6304
  Copyright terms: Public domain W3C validator