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

Theorem riotaex 6261
Description: Restricted iota is a set. (Contributed by NM, 15-Sep-2011.)
Assertion
Ref Expression
riotaex

Proof of Theorem riotaex
StepHypRef Expression
1 df-riota 6257 . 2
2 iotaex 5573 . 2
31, 2eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818   cvv 3109  iotacio 5554  iota_crio 6256
This theorem is referenced by:  ordtypelem3  7966  dfac8clem  8434  zorn2lem1  8897  subval  9834  1div0  10233  divval  10234  elq  11213  flval  11931  ceilval2  11969  cjval  12935  sqrtval  13070  sqrtf  13196  cidval  15074  cidfn  15076  lubdm  15609  lubval  15614  glbdm  15622  glbval  15627  grpinvval  16089  grpinvfn  16090  pj1val  16713  evlsval  18188  q1pval  22554  ig1pval  22573  coeval  22620  quotval  22688  mirfv  24037  mirf  24041  usgraidx2v  24393  nbgraf1olem4  24444  frgrancvvdeqlem6  25035  1div0apr  25176  gidval  25215  fngid  25216  grpoinvval  25227  grpoinvf  25242  pjhval  26315  pjfni  26619  cnlnadjlem5  26990  nmopadjlei  27007  cdj3lem2  27354  xdivval  27615  cvmlift3lem4  28767  fvtransport  29682  mpaaval  31100  usgedgvadf1  32415  usgedgvadf1ALT  32418  lshpkrlem1  34835  lshpkrlem2  34836  lshpkrlem3  34837  trlval  35887  cdleme31fv  36116  cdleme50f  36268  cdlemksv  36570  cdlemkuu  36621  cdlemk40  36643  cdlemk56  36697  cdlemm10N  36845  cdlemn11a  36934  dihval  36959  dihf11lem  36993  dihatlat  37061  dochfl1  37203  mapdhval  37451  hvmapvalvalN  37488  hdmap1vallem  37525  hdmapval  37558  hdmapfnN  37559  hgmapval  37617  hgmapfnN  37618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556  df-riota 6257
  Copyright terms: Public domain W3C validator