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

Theorem riotaex 6310
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 6306 . 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 5238 . . 3  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
3 fvex 5541 . . 3  |-  ( Undef `  { x  |  x  e.  A } )  e.  _V
42, 3ifex 3625 . 2  |-  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps )
) ,  ( Undef `  { x  |  x  e.  A } ) )  e.  _V
51, 4eqeltri 2355 1  |-  ( iota_ x  e.  A ps )  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 358    e. wcel 1686   {cab 2271   E!wreu 2547   _Vcvv 2790   ifcif 3567   iotacio 5219   ` cfv 5257   Undefcund 6298   iota_crio 6299
This theorem is referenced by:  ordtypelem3  7237  dfac8clem  7661  zorn2lem1  8125  subval  9045  1div0  9427  divval  9428  elq  10320  flval  10928  cjval  11589  sqrval  11724  sqrf  11849  cidval  13581  cidfn  13583  lubval  14115  glbval  14120  spwval2  14335  grpinvval  14523  grpinvfn  14524  pj1val  15006  evlsval  19405  q1pval  19541  ig1pval  19560  coeval  19607  quotval  19674  1div0apr  20843  gidval  20882  fngid  20883  grpoinvval  20894  grpoinvf  20909  pjhval  21978  pjfni  22282  cnlnadjlem5  22653  nmopadjlei  22670  cdj3lem2  23017  xdivval  23104  cvmlift3lem4  23855  fvtransport  24657  issubcv  25681  lineval222  26090  lineval3a  26094  mpaaval  27367  lshpkrlem1  29373  lshpkrlem2  29374  lshpkrlem3  29375  trlval  30424  cdleme31fv  30652  cdleme50f  30804  cdlemksv  31106  cdlemkuu  31157  cdlemk40  31179  cdlemk56  31233  cdlemm10N  31381  cdlemn11a  31470  dihval  31495  dihf11lem  31529  dihatlat  31597  dochfl1  31739  mapdhval  31987  hvmapvalvalN  32024  hdmap1vallem  32061  hdmapval  32094  hdmapfnN  32095  hgmapval  32153  hgmapfnN  32154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-nul 4151
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-uni 3830  df-iota 5221  df-fv 5265  df-riota 6306
  Copyright terms: Public domain W3C validator