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

Theorem riotaex 6051
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 6047 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5393 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2508 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1756   _Vcvv 2967   iotacio 5374   iota_crio 6046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-sn 3873  df-pr 3875  df-uni 4087  df-iota 5376  df-riota 6047
This theorem is referenced by:  ordtypelem3  7726  dfac8clem  8194  zorn2lem1  8657  subval  9593  1div0  9987  divval  9988  elq  10947  flval  11636  ceilval2  11673  cjval  12583  sqrval  12718  sqrf  12843  cidval  14607  cidfn  14609  lubdm  15141  lubval  15146  glbdm  15154  glbval  15159  grpinvval  15568  grpinvfn  15569  pj1val  16183  evlsval  17580  q1pval  21600  ig1pval  21619  coeval  21666  quotval  21733  mirfv  23028  mircl  23032  usgraidx2v  23262  nbgraf1olem4  23304  1div0apr  23612  gidval  23651  fngid  23652  grpoinvval  23663  grpoinvf  23678  pjhval  24751  pjfni  25055  cnlnadjlem5  25426  nmopadjlei  25443  cdj3lem2  25790  xdivval  26045  cvmlift3lem4  27163  fvtransport  28014  mpaaval  29461  frgrancvvdeqlem6  30581  lshpkrlem1  32595  lshpkrlem2  32596  lshpkrlem3  32597  trlval  33646  cdleme31fv  33874  cdleme50f  34026  cdlemksv  34328  cdlemkuu  34379  cdlemk40  34401  cdlemk56  34455  cdlemm10N  34603  cdlemn11a  34692  dihval  34717  dihf11lem  34751  dihatlat  34819  dochfl1  34961  mapdhval  35209  hvmapvalvalN  35246  hdmap1vallem  35283  hdmapval  35316  hdmapfnN  35317  hgmapval  35375  hgmapfnN  35376
  Copyright terms: Public domain W3C validator