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

Theorem riotaex 6164
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 6160 . 2  |-  ( iota_ x  e.  A  ps )  =  ( iota x
( x  e.  A  /\  ps ) )
2 iotaex 5505 . 2  |-  ( iota
x ( x  e.  A  /\  ps )
)  e.  _V
31, 2eqeltri 2538 1  |-  ( iota_ x  e.  A  ps )  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    e. wcel 1758   _Vcvv 3076   iotacio 5486   iota_crio 6159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-sn 3985  df-pr 3987  df-uni 4199  df-iota 5488  df-riota 6160
This theorem is referenced by:  ordtypelem3  7844  dfac8clem  8312  zorn2lem1  8775  subval  9711  1div0  10105  divval  10106  elq  11065  flval  11760  ceilval2  11797  cjval  12708  sqrval  12843  sqrf  12968  cidval  14733  cidfn  14735  lubdm  15267  lubval  15272  glbdm  15280  glbval  15285  grpinvval  15695  grpinvfn  15696  pj1val  16312  evlsval  17728  q1pval  21757  ig1pval  21776  coeval  21823  quotval  21890  mirfv  23202  mirf  23206  usgraidx2v  23462  nbgraf1olem4  23504  1div0apr  23812  gidval  23851  fngid  23852  grpoinvval  23863  grpoinvf  23878  pjhval  24951  pjfni  25255  cnlnadjlem5  25626  nmopadjlei  25643  cdj3lem2  25990  xdivval  26238  cvmlift3lem4  27354  fvtransport  28206  mpaaval  29655  frgrancvvdeqlem6  30775  lshpkrlem1  33078  lshpkrlem2  33079  lshpkrlem3  33080  trlval  34129  cdleme31fv  34357  cdleme50f  34509  cdlemksv  34811  cdlemkuu  34862  cdlemk40  34884  cdlemk56  34938  cdlemm10N  35086  cdlemn11a  35175  dihval  35200  dihf11lem  35234  dihatlat  35302  dochfl1  35444  mapdhval  35692  hvmapvalvalN  35729  hdmap1vallem  35766  hdmapval  35799  hdmapfnN  35800  hgmapval  35858  hgmapfnN  35859
  Copyright terms: Public domain W3C validator