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

Theorem riotabidv 6259
Description: Formula-building deduction rule for restricted iota. (Contributed by NM, 15-Sep-2011.)
Hypothesis
Ref Expression
riotabidv.1
Assertion
Ref Expression
riotabidv
Distinct variable group:   ,

Proof of Theorem riotabidv
StepHypRef Expression
1 riotabidv.1 . . . 4
21anbi2d 703 . . 3
32iotabidv 5577 . 2
4 df-riota 6257 . 2
5 df-riota 6257 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  iotacio 5554  iota_crio 6256
This theorem is referenced by:  riotaeqbidv  6260  csbriota  6269  fin23lem27  8729  subval  9834  divval  10234  flval  11931  ceilval2  11969  cjval  12935  sqrtval  13070  qnumval  14270  qdenval  14271  lubval  15614  glbval  15627  joinval2  15639  meetval2  15653  grpinvval  16089  pj1fval  16712  pj1val  16713  q1pval  22554  coeval  22620  quotval  22688  ismidb  24144  lmif  24151  islmib  24153  usgraidx2v  24393  nbgraf1olem4  24444  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  grpoinvval  25227  pjhval  26315  nmopadjlei  27007  cdj3lem2  27354  cvmliftlem15  28743  cvmlift2lem4  28751  cvmlift2  28761  cvmlift3lem2  28765  cvmlift3lem4  28767  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  cvmlift3  28773  fvtransport  29682  unxpwdom3  31041  mpaaval  31100  usgedgvadf1  32415  usgedgvadf1ALT  32418  lshpkrlem1  34835  lshpkrlem2  34836  lshpkrlem3  34837  lshpkrcl  34841  trlset  35886  trlval  35887  cdleme27b  36094  cdleme29b  36101  cdleme31so  36105  cdleme31sn1  36107  cdleme31sn1c  36114  cdleme31fv  36116  cdlemefrs29clN  36125  cdleme40v  36195  cdlemg1cN  36313  cdlemg1cex  36314  cdlemksv  36570  cdlemkuu  36621  cdlemkid3N  36659  cdlemkid4  36660  cdlemm10N  36845  dicval  36903  dihval  36959  dochfl1  37203  lcfl7N  37228  lcfrlem8  37276  lcfrlem9  37277  lcf1o  37278  mapdhval  37451  hvmapval  37487  hvmapvalvalN  37488  hdmap1fval  37524  hdmap1vallem  37525  hdmap1val  37526  hdmap1cbv  37530  hdmapfval  37557  hdmapval  37558  hgmapffval  37615  hgmapfval  37616  hgmapval  37617
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
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-uni 4250  df-iota 5556  df-riota 6257
  Copyright terms: Public domain W3C validator