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

Theorem riotaex 6520
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 6516 . 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 5402 . . 3  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
3 fvex 5709 . . 3  |-  ( Undef `  { x  |  x  e.  A } )  e.  _V
42, 3ifex 3765 . 2  |-  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps )
) ,  ( Undef `  { x  |  x  e.  A } ) )  e.  _V
51, 4eqeltri 2482 1  |-  ( iota_ x  e.  A ps )  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1721   {cab 2398   E!wreu 2676   _Vcvv 2924   ifcif 3707   iotacio 5383   ` cfv 5421   Undefcund 6508   iota_crio 6509
This theorem is referenced by:  ordtypelem3  7453  dfac8clem  7877  zorn2lem1  8340  subval  9261  1div0  9643  divval  9644  elq  10540  flval  11166  cjval  11870  sqrval  12005  sqrf  12130  cidval  13865  cidfn  13867  lubval  14399  glbval  14404  spwval2  14619  grpinvval  14807  grpinvfn  14808  pj1val  15290  evlsval  19901  q1pval  20037  ig1pval  20056  coeval  20103  quotval  20170  usgraidx2v  21373  nbgraf1olem4  21415  1div0apr  21723  gidval  21762  fngid  21763  grpoinvval  21774  grpoinvf  21789  pjhval  22860  pjfni  23164  cnlnadjlem5  23535  nmopadjlei  23552  cdj3lem2  23899  xdivval  24126  cvmlift3lem4  24970  fvtransport  25878  mpaaval  27232  frgrancvvdeqlem6  28146  lshpkrlem1  29605  lshpkrlem2  29606  lshpkrlem3  29607  trlval  30656  cdleme31fv  30884  cdleme50f  31036  cdlemksv  31338  cdlemkuu  31389  cdlemk40  31411  cdlemk56  31465  cdlemm10N  31613  cdlemn11a  31702  dihval  31727  dihf11lem  31761  dihatlat  31829  dochfl1  31971  mapdhval  32219  hvmapvalvalN  32256  hdmap1vallem  32293  hdmapval  32326  hdmapfnN  32327  hgmapval  32385  hgmapfnN  32386
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-nul 4306
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-uni 3984  df-iota 5385  df-fv 5429  df-riota 6516
  Copyright terms: Public domain W3C validator