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

Theorem riotaex 6243
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 6239 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5549 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2486 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367    e. wcel 1842   _Vcvv 3058   iotacio 5530   iota_crio 6238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-nul 4524
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-v 3060  df-sbc 3277  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-sn 3972  df-pr 3974  df-uni 4191  df-iota 5532  df-riota 6239
This theorem is referenced by:  ordtypelem3  7978  dfac8clem  8444  zorn2lem1  8907  subval  9846  1div0  10248  divval  10249  elq  11228  flval  11966  ceilval2  12005  cjval  13082  sqrtval  13217  sqrtf  13343  cidval  15289  cidfn  15291  lubdm  15931  lubval  15936  glbdm  15944  glbval  15949  grpinvval  16411  grpinvfn  16412  pj1val  17035  evlsval  18506  q1pval  22844  ig1pval  22863  coeval  22910  quotval  22978  mirfv  24420  mirf  24424  usgraidx2v  24797  nbgraf1olem4  24848  frgrancvvdeqlem6  25439  1div0apr  25580  gidval  25615  fngid  25616  grpoinvval  25627  grpoinvf  25642  pjhval  26715  pjfni  27019  cnlnadjlem5  27389  nmopadjlei  27406  cdj3lem2  27753  xdivval  28053  cvmlift3lem4  29606  fvtransport  30357  lshpkrlem1  32108  lshpkrlem2  32109  lshpkrlem3  32110  trlval  33160  cdleme31fv  33389  cdleme50f  33541  cdlemksv  33843  cdlemkuu  33894  cdlemk40  33916  cdlemk56  33970  cdlemm10N  34118  cdlemn11a  34207  dihval  34232  dihf11lem  34266  dihatlat  34334  dochfl1  34476  mapdhval  34724  hvmapvalvalN  34761  hdmap1vallem  34798  hdmapval  34831  hdmapfnN  34832  hgmapval  34890  hgmapfnN  34891  mpaaval  35444  usgedgvadf1  38025  usgedgvadf1ALT  38028
  Copyright terms: Public domain W3C validator