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

Theorem riotacl 6531
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 3396 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 6530 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3314 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 1721   E!wreu 2676   {crab 2678   iota_crio 6509
This theorem is referenced by:  riotaprop  6540  riotass2  6544  riotass  6545  riotaxfrd  6548  riotaclbg  6556  riotaundb  6558  supcl  7427  fisupcl  7436  htalem  7784  dfac8clem  7877  dfac2a  7974  fin23lem22  8171  zorn2lem1  8340  subcl  9269  divcl  9648  lbcl  9923  flcl  11167  cjf  11872  sqrcl  12128  qnumdencl  13094  qnumdenbi  13099  catidcl  13870  ismgmid  14673  grpinvf  14812  pj1f  15292  usgraidx2vlem1  21371  nbgraf1olem2  21413  grpoidcl  21766  grpoinvcl  21775  iorlid  21877  pjpreeq  22861  cnlnadjlem3  23533  adjbdln  23547  xdivcld  24130  cvmlift3lem3  24969  transportcl  25879  frgrancvvdeqlem5  28145  lshpkrlem2  29606  lshpkrcl  29611  dihlsscpre  31729  mapdhcl  32222  hdmapcl  32328  hgmapcl  32387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-un 3293  df-in 3295  df-ss 3302  df-if 3708  df-sn 3788  df-pr 3789  df-uni 3984  df-iota 5385  df-riota 6516
  Copyright terms: Public domain W3C validator