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

Theorem riotaex 6556
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 6552 . 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 5438 . . 3  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
3 fvex 5745 . . 3  |-  ( Undef `  { x  |  x  e.  A } )  e.  _V
42, 3ifex 3799 . 2  |-  if ( E! x  e.  A  ps ,  ( iota x ( x  e.  A  /\  ps )
) ,  ( Undef `  { x  |  x  e.  A } ) )  e.  _V
51, 4eqeltri 2508 1  |-  ( iota_ x  e.  A ps )  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 360    e. wcel 1726   {cab 2424   E!wreu 2709   _Vcvv 2958   ifcif 3741   iotacio 5419   ` cfv 5457   Undefcund 6544   iota_crio 6545
This theorem is referenced by:  ordtypelem3  7492  dfac8clem  7918  zorn2lem1  8381  subval  9302  1div0  9684  divval  9685  elq  10581  flval  11208  cjval  11912  sqrval  12047  sqrf  12172  cidval  13907  cidfn  13909  lubval  14441  glbval  14446  spwval2  14661  grpinvval  14849  grpinvfn  14850  pj1val  15332  evlsval  19945  q1pval  20081  ig1pval  20100  coeval  20147  quotval  20214  usgraidx2v  21417  nbgraf1olem4  21459  1div0apr  21767  gidval  21806  fngid  21807  grpoinvval  21818  grpoinvf  21833  pjhval  22904  pjfni  23208  cnlnadjlem5  23579  nmopadjlei  23596  cdj3lem2  23943  xdivval  24170  cvmlift3lem4  25014  fvtransport  25971  mpaaval  27347  frgrancvvdeqlem6  28498  lshpkrlem1  29982  lshpkrlem2  29983  lshpkrlem3  29984  trlval  31033  cdleme31fv  31261  cdleme50f  31413  cdlemksv  31715  cdlemkuu  31766  cdlemk40  31788  cdlemk56  31842  cdlemm10N  31990  cdlemn11a  32079  dihval  32104  dihf11lem  32138  dihatlat  32206  dochfl1  32348  mapdhval  32596  hvmapvalvalN  32633  hdmap1vallem  32670  hdmapval  32703  hdmapfnN  32704  hgmapval  32762  hgmapfnN  32763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4341
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-uni 4018  df-iota 5421  df-fv 5465  df-riota 6552
  Copyright terms: Public domain W3C validator