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

Theorem riotacl 5482
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 3025 . 2  |-  { x  e.  A  |  ph }  C_  A
2 riotacl2 5481 . 2  |-  ( E! x  e.  A  ph  ->  ( iota_ x  e.  A  ph )  e.  { x  e.  A  |  ph }
)
31, 2sseldi 2943 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 1393   E!wreu 2308   {crab 2310   iota_crio 5467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-un 2922  df-in 2924  df-ss 2931  df-sn 3381  df-pr 3382  df-uni 3581  df-iota 4867  df-riota 5468
This theorem is referenced by:  riotaprop  5491  riotass2  5494  riotass  5495  acexmidlemcase  5507  caucvgsrlemcl  6873  caucvgsrlemgt1  6879  axcaucvglemcl  6969  subval  7203  subcl  7210  divvalap  7653  divclap  7657  divfnzn  8556  flqcl  9117  cjval  9445  cjth  9446  cjf  9447
  Copyright terms: Public domain W3C validator