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

Theorem riotaex 6308
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 6304 . 2  |-  ( iota_ x  e.  A ps )  =  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps ) ) ,  (
Undef `  { x  |  x  e.  A }
) )
2 iotaex 5236 . . 3  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
3 fvex 5539 . . 3  |-  ( Undef `  { x  |  x  e.  A } )  e.  _V
42, 3ifex 3623 . 2  |-  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps )
) ,  ( Undef `  { x  |  x  e.  A } ) )  e.  _V
51, 4eqeltri 2353 1  |-  ( iota_ x  e.  A ps )  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1684   {cab 2269   E!wreu 2545   _Vcvv 2788   ifcif 3565   iotacio 5217   ` cfv 5255   Undefcund 6296   iota_crio 6297
This theorem is referenced by:  ordtypelem3  7235  dfac8clem  7659  zorn2lem1  8123  subval  9043  1div0  9425  divval  9426  elq  10318  flval  10926  cjval  11587  sqrval  11722  sqrf  11847  cidval  13579  cidfn  13581  lubval  14113  glbval  14118  spwval2  14333  grpinvval  14521  grpinvfn  14522  pj1val  15004  evlsval  19403  q1pval  19539  ig1pval  19558  coeval  19605  quotval  19672  1div0apr  20841  gidval  20880  fngid  20881  grpoinvval  20892  grpoinvf  20907  pjhval  21976  pjfni  22280  cnlnadjlem5  22651  nmopadjlei  22668  cdj3lem2  23015  xdivval  23102  cvmlift3lem4  23853  fvtransport  24655  issubcv  25670  lineval222  26079  lineval3a  26083  mpaaval  27356  lshpkrlem1  29300  lshpkrlem2  29301  lshpkrlem3  29302  trlval  30351  cdleme31fv  30579  cdleme50f  30731  cdlemksv  31033  cdlemkuu  31084  cdlemk40  31106  cdlemk56  31160  cdlemm10N  31308  cdlemn11a  31397  dihval  31422  dihf11lem  31456  dihatlat  31524  dochfl1  31666  mapdhval  31914  hvmapvalvalN  31951  hdmap1vallem  31988  hdmapval  32021  hdmapfnN  32022  hgmapval  32080  hgmapfnN  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-uni 3828  df-iota 5219  df-fv 5263  df-riota 6304
  Copyright terms: Public domain W3C validator