ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  riotacl Unicode version

Theorem riotacl 5712
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 3152 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 5711 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 3065 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 1465   E!wreu 2395   {crab 2397   iota_crio 5697
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-eu 1980  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-reu 2400  df-rab 2402  df-v 2662  df-sbc 2883  df-un 3045  df-in 3047  df-ss 3054  df-sn 3503  df-pr 3504  df-uni 3707  df-iota 5058  df-riota 5698
This theorem is referenced by:  riotaprop  5721  riotass2  5724  riotass  5725  acexmidlemcase  5737  supclti  6853  caucvgsrlemcl  7565  caucvgsrlemgt1  7571  axcaucvglemcl  7671  subval  7922  subcl  7929  divvalap  8402  divclap  8406  lbcl  8672  divfnzn  9381  flqcl  10014  flapcl  10016  cjval  10585  cjth  10586  cjf  10587  oddpwdclemodd  11777  oddpwdclemdc  11778  oddpwdc  11779  qnumdencl  11792  qnumdenbi  11797
  Copyright terms: Public domain W3C validator