Theorem riotaex 6615

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

Step	Hyp	Ref	Expression
1		df-riota 6611	. 2 |- ( iota_ x e. A ps ) = ( iota x ( x e. A /\ ps ) )
2		iotaex 5868	. 2 |- ( iota x ( x e. A /\ ps ) ) e. _V
3	1, 2	eqeltri 2697	1 |- ( iota_ x e. A ps ) e. _V

Syntax hints:   /\ wa 384   e. wcel 1990   _Vcvv 3200   iotacio 5849   iota_crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  ordtypelem3  8425  dfac8clem  8855  zorn2lem1  9318  subval  10272  1div0  10686  divval  10687  elq  11790  flval  12595  ceilval2  12641  cjval  13842  sqrtval  13977  sqrtf  14103  cidval  16338  cidfn  16340  lubdm  16979  lubval  16984  glbdm  16992  glbval  16997  grpinvval  17461  grpinvfn  17462  pj1val  18108  evlsval  19519  q1pval  23913  ig1pval  23932  coeval  23979  quotval  24047  mirfv  25551  mirf  25555  usgredg2v  26119  frgrncvvdeqlem5  27167  1div0apr  27324  gidval  27366  grpoinvval  27377  grpoinvf  27386  pjhval  28256  pjfni  28560  cnlnadjlem5  28930  nmopadjlei  28947  cdj3lem2  29294  xdivval  29627  cvmlift3lem4  31304  scutval  31911  dmscut  31918  fvtransport  32139  finxpreclem4  33231  poimirlem26  33435  lshpkrlem1  34397  lshpkrlem2  34398  lshpkrlem3  34399  trlval  35449  cdleme31fv  35678  cdleme50f  35830  cdlemksv  36132  cdlemkuu  36183  cdlemk40  36205  cdlemk56  36259  cdlemm10N  36407  cdlemn11a  36496  dihval  36521  dihf11lem  36555  dihatlat  36623  dochfl1  36765  mapdhval  37013  hvmapvalvalN  37050  hdmap1vallem  37087  hdmapval  37120  hdmapfnN  37121  hgmapval  37179  hgmapfnN  37180  mpaaval  37721  wessf1ornlem  39371