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

Theorem riota5 6283
Description: A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)
Hypotheses
Ref Expression
riota5.1
riota5.2
Assertion
Ref Expression
riota5
Distinct variable groups:   ,   ,   ,

Proof of Theorem riota5
StepHypRef Expression
1 nfcvd 2620 . 2
2 riota5.1 . 2
3 riota5.2 . 2
41, 2, 3riota5f 6282 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  iota_crio 6256
This theorem is referenced by:  f1ocnvfv3  6292  sqrt0  13075  lubid  15620  lubun  15753  odval2  16575  adjvalval  26856  xdivpnfrp  27629  xrsinvgval  27665  unxpwdom3  31041  lub0N  34914  glb0N  34918  trlval2  35888  cdlemefrs32fva  36126  cdleme32fva  36163  cdlemg1a  36296
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-or 370  df-an 371  df-3an 975  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-ral 2812  df-rex 2813  df-reu 2814  df-v 3111  df-sbc 3328  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556  df-riota 6257
  Copyright terms: Public domain W3C validator