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

Theorem riota5 7410
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 2893 . 2 (𝜑𝑥𝐵)
2 riota5.1 . 2 (𝜑𝐵𝐴)
3 riota5.2 . 2 ((𝜑𝑥𝐴) → (𝜓𝑥 = 𝐵))
41, 2, 3riota5f 7409 1 (𝜑 → (𝑥𝐴 𝜓) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1534  wcel 2099  crio 7379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-reu 3365  df-v 3464  df-sbc 3777  df-un 3952  df-ss 3964  df-sn 4634  df-pr 4636  df-uni 4914  df-iota 6506  df-riota 7380
This theorem is referenced by:  f1ocnvfv3  7419  ttrcltr  9759  sqrt0  15246  lubid  18387  lubun  18540  odval2  19549  adjvalval  31870  xdivpnfrp  32794  xrsinvgval  32888  dfgcd3  37031  poimirlem6  37327  poimirlem7  37328  lub0N  38887  glb0N  38891  trlval2  39862  cdlemefrs32fva  40099  cdleme32fva  40136  cdlemg1a  40269  unxpwdom3  42756
  Copyright terms: Public domain W3C validator