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

Theorem riota5 6779
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:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem riota5
StepHypRef Expression
1 nfcvd 2913 . 2 (𝜑𝑥𝐵)
2 riota5.1 . 2 (𝜑𝐵𝐴)
3 riota5.2 . 2 ((𝜑𝑥𝐴) → (𝜓𝑥 = 𝐵))
41, 2, 3riota5f 6778 1 (𝜑 → (𝑥𝐴 𝜓) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1630  wcel 2144  crio 6752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-reu 3067  df-v 3351  df-sbc 3586  df-un 3726  df-sn 4315  df-pr 4317  df-uni 4573  df-iota 5994  df-riota 6753
This theorem is referenced by:  f1ocnvfv3  6788  sqrt0  14189  lubid  17197  lubun  17330  odval2  18176  adjvalval  29130  xdivpnfrp  29975  xrsinvgval  30011  dfgcd3  33500  poimirlem6  33741  poimirlem7  33742  lub0N  34991  glb0N  34995  trlval2  35965  cdlemefrs32fva  36202  cdleme32fva  36239  cdlemg1a  36372  unxpwdom3  38184
  Copyright terms: Public domain W3C validator