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

Theorem riotaex 6268
Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
riotaex  |-  ( iota_ x  e.  A  ps )  e.  _V

Proof of Theorem riotaex
StepHypRef Expression
1 df-riota 6264 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5579 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2506 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    e. wcel 1868   _Vcvv 3081   iotacio 5560   iota_crio 6263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-nul 4552
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-sn 3997  df-pr 3999  df-uni 4217  df-iota 5562  df-riota 6264
This theorem is referenced by:  ordtypelem3  8038  dfac8clem  8464  zorn2lem1  8927  subval  9867  1div0  10272  divval  10273  elq  11267  flval  12030  ceilval2  12069  cjval  13154  sqrtval  13289  sqrtf  13415  cidval  15571  cidfn  15573  lubdm  16213  lubval  16218  glbdm  16226  glbval  16231  grpinvval  16693  grpinvfn  16694  pj1val  17333  evlsval  18730  q1pval  23091  ig1pval  23111  ig1pvalOLD  23117  coeval  23164  quotval  23232  mirfv  24688  mirf  24692  usgraidx2v  25107  nbgraf1olem4  25158  frgrancvvdeqlem6  25749  1div0apr  25891  gidval  25927  fngid  25928  grpoinvval  25939  grpoinvf  25954  pjhval  27036  pjfni  27340  cnlnadjlem5  27710  nmopadjlei  27727  cdj3lem2  28074  xdivval  28383  cvmlift3lem4  30041  fvtransport  30792  poimirlem26  31880  lshpkrlem1  32595  lshpkrlem2  32596  lshpkrlem3  32597  trlval  33647  cdleme31fv  33876  cdleme50f  34028  cdlemksv  34330  cdlemkuu  34381  cdlemk40  34403  cdlemk56  34457  cdlemm10N  34605  cdlemn11a  34694  dihval  34719  dihf11lem  34753  dihatlat  34821  dochfl1  34963  mapdhval  35211  hvmapvalvalN  35248  hdmap1vallem  35285  hdmapval  35318  hdmapfnN  35319  hgmapval  35377  hgmapfnN  35378  mpaaval  35937  wessf1ornlem  37309  usgridx2v  38930  usgedgvadf1  38999  usgedgvadf1ALT  39002
  Copyright terms: Public domain W3C validator