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

Theorem riotaex 6247
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 6243 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5566 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2551 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1767   _Vcvv 3113   iotacio 5547   iota_crio 6242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-sn 4028  df-pr 4030  df-uni 4246  df-iota 5549  df-riota 6243
This theorem is referenced by:  ordtypelem3  7941  dfac8clem  8409  zorn2lem1  8872  subval  9807  1div0  10204  divval  10205  elq  11180  flval  11895  ceilval2  11932  cjval  12892  sqrtval  13027  sqrtf  13152  cidval  14925  cidfn  14927  lubdm  15459  lubval  15464  glbdm  15472  glbval  15477  grpinvval  15887  grpinvfn  15888  pj1val  16506  evlsval  17956  q1pval  22286  ig1pval  22305  coeval  22352  quotval  22419  mirfv  23747  mirf  23751  usgraidx2v  24066  nbgraf1olem4  24117  frgrancvvdeqlem6  24709  1div0apr  24849  gidval  24888  fngid  24889  grpoinvval  24900  grpoinvf  24915  pjhval  25988  pjfni  26292  cnlnadjlem5  26663  nmopadjlei  26680  cdj3lem2  27027  xdivval  27280  cvmlift3lem4  28404  fvtransport  29256  mpaaval  30705  usgedgvadf1  31884  usgedgvadf1ALT  31887  lshpkrlem1  33907  lshpkrlem2  33908  lshpkrlem3  33909  trlval  34958  cdleme31fv  35186  cdleme50f  35338  cdlemksv  35640  cdlemkuu  35691  cdlemk40  35713  cdlemk56  35767  cdlemm10N  35915  cdlemn11a  36004  dihval  36029  dihf11lem  36063  dihatlat  36131  dochfl1  36273  mapdhval  36521  hvmapvalvalN  36558  hdmap1vallem  36595  hdmapval  36628  hdmapfnN  36629  hgmapval  36687  hgmapfnN  36688
  Copyright terms: Public domain W3C validator