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

Theorem riotaex 6262
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 6258 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5574 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2541 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1819   _Vcvv 3109   iotacio 5555   iota_crio 6257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-sn 4033  df-pr 4035  df-uni 4252  df-iota 5557  df-riota 6258
This theorem is referenced by:  ordtypelem3  7963  dfac8clem  8430  zorn2lem1  8893  subval  9830  1div0  10229  divval  10230  elq  11209  flval  11934  ceilval2  11972  cjval  12947  sqrtval  13082  sqrtf  13208  cidval  15094  cidfn  15096  lubdm  15736  lubval  15741  glbdm  15749  glbval  15754  grpinvval  16216  grpinvfn  16217  pj1val  16840  evlsval  18315  q1pval  22680  ig1pval  22699  coeval  22746  quotval  22814  mirfv  24163  mirf  24167  usgraidx2v  24520  nbgraf1olem4  24571  frgrancvvdeqlem6  25162  1div0apr  25303  gidval  25342  fngid  25343  grpoinvval  25354  grpoinvf  25369  pjhval  26442  pjfni  26746  cnlnadjlem5  27117  nmopadjlei  27134  cdj3lem2  27481  xdivval  27775  cvmlift3lem4  28964  fvtransport  29887  mpaaval  31304  usgedgvadf1  32677  usgedgvadf1ALT  32680  lshpkrlem1  34978  lshpkrlem2  34979  lshpkrlem3  34980  trlval  36030  cdleme31fv  36259  cdleme50f  36411  cdlemksv  36713  cdlemkuu  36764  cdlemk40  36786  cdlemk56  36840  cdlemm10N  36988  cdlemn11a  37077  dihval  37102  dihf11lem  37136  dihatlat  37204  dochfl1  37346  mapdhval  37594  hvmapvalvalN  37631  hdmap1vallem  37668  hdmapval  37701  hdmapfnN  37702  hgmapval  37760  hgmapfnN  37761
  Copyright terms: Public domain W3C validator